have : α = β := funext fun n => by
  suffices ∃ (a : α n) (b : β n), HEq a b
  from let ⟨_,_,hab⟩ := this; type_eq_of_heq hab
  induction n with
  | zero => exact ⟨a,b,hab⟩
  | succ n IH =>
    let ⟨a,b,hab⟩ := IH
    exact ⟨f n a, g n b, hfg n a b hab⟩
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
this : α = β
⊢ HEq (dfold f n a) (dfold g n b)