case inr.inl
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x
α : Type u_1
P : α → Prop
x : α
⊢ Any P {x} → P x
rintro (⟨⟨⟩⟩ | h | ⟨⟨⟩⟩)
no goals
case inr.inl
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x
exact h