suffices ∃ (a : α n) (b : β n), HEq a b
from let ⟨_,_,hab⟩ := this; type_eq_of_heq 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
n : Nat
⊢ α n = β n
α β : 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
n : Nat
⊢ ∃ a b, HEq a b