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