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

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

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