case refl
α✝ : Sort u_1
x : α✝
p : HEq x x → Prop
h : ∀ (he : x = x), p (_ : HEq x x)
⊢ p (_ : HEq x x)
α✝ : Sort u_1
x y : α✝
p : HEq x y → Prop
h : ∀ (he : x = y), p (_ : HEq x y)
he : HEq x y
⊢ p he
cases he
no goals
case refl
α✝ : Sort u_1
x : α✝
p : HEq x x → Prop
h : ∀ (he : x = x), p (_ : HEq x x)
⊢ p (_ : HEq x x)
exact h rfl