Let alpha and p be given.
Assume H1.
Apply PNoLtE alpha alpha p p H1 to the current goal.
Assume H1: PNoLt_ (alpha ∩ alpha) p p.
An exact proof term for the current goal is PNoLt_irref_ (alpha ∩ alpha) p H1.
Assume H1: alpha ∈ alpha.
We will prove False.
An exact proof term for the current goal is In_irref alpha H1.
Assume H1: alpha ∈ alpha.
We will prove False.
An exact proof term for the current goal is In_irref alpha H1.
∎