Theorem: Container.Eq_from_Heq (CoInd/M.lean)

State before:
C : Container
α β : Sort u₁
i : α
j : β
h₀ : α = β
h : HEq i j
⊢ cast h₀ i = j
Tactic:
cases h
State after:
case refl
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ cast h₀ i = i

State before:
case refl
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ cast h₀ i = i
Tactic:
apply eq_of_heq
State after:
case refl.h
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ HEq (cast h₀ i) i

State before:
case refl.h
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ HEq (cast h₀ i) i
Tactic:
apply cast_heq
State after:
no goals