Theorem: eqNdrec_eq_cast (GMLInit/Logic/Cast.lean)

State before:
α : Sort u_1
a b : α
motive : α → Sort u_2
t : motive a
h : a = b
⊢ h ▸ t = cast ⋯ t
Tactic:
cases h
State after:
case refl
α : Sort u_1
a : α
motive : α → Sort u_2
t : motive a
⊢ ⋯ ▸ t = cast ⋯ t

State before:
case refl
α : Sort u_1
a : α
motive : α → Sort u_2
t : motive a
⊢ ⋯ ▸ t = cast ⋯ t
Tactic:
rfl
State after:
no goals