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

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

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