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

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

State before:
case refl
α : Sort u_1
β : α → Sort u_2
a : α
x : β a
⊢ ⋯ ▸ x ≅ x
Tactic:
exact HEq.rfl
State after:
no goals