Theorem: HEq.heq_eqNdrec_iff_heq (GMLInit/Logic/HEq.lean)

State before:
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a a' : α
h : a = a'
x : β a
y : γ
⊢ y ≅ h ▸ x ↔ y ≅ x
Tactic:
cases h
State after:
case refl
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a : α
x : β a
y : γ
⊢ y ≅ ⋯ ▸ x ↔ y ≅ x

State before:
case refl
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a : α
x : β a
y : γ
⊢ y ≅ ⋯ ▸ x ↔ y ≅ x
Tactic:
exact Iff.rfl
State after:
no goals