case refl
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p (_ : x = x)
⊢ p (_ : x = x)
x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p (_ : x = y)
he : x = y
⊢ p he
cases he
no goals
case refl
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p (_ : x = x)
⊢ p (_ : x = x)
exact h Iff.rfl