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

State before:
α β γ : Sort u_1
h : α = β
x : α
y : γ
⊢ y ≅ cast h x ↔ y ≅ x
Tactic:
cases h
State after:
case refl
α γ : Sort u_1
x : α
y : γ
⊢ y ≅ cast ⋯ x ↔ y ≅ x

State before:
case refl
α γ : Sort u_1
x : α
y : γ
⊢ y ≅ cast ⋯ x ↔ y ≅ x
Tactic:
exact Iff.rfl
State after:
no goals