simplify an equiv

Stream: new members

[Horatiu Cheval]

I need to prove the equiv below involving lots of singleton types.
I know I can do it by hand with repeated applications of equivs for products, functions and units, equiv_rewrites and things like this (I am not asking for someone to do the dirty work for me),
but I am wondering whether some tactic or automation exist that could save me from doing that.

import data.equiv.basic

  example (α β γ δ ε: Type*) [unique β] [unique γ] [unique δ] [unique ε]
  : (α → ((ℕ → β) → (ℕ → γ → δ) → (Σ (x_1 : ℕ), ε)) × ((ℕ → β) → (Σ (x_1 : ℕ), γ))) ≃
  (α → ℕ × ℕ)

[Yakov Pechersky]

Likely, suggest.

[Yakov Pechersky]

Or repeated usage of suggest