Let alpha, beta, p and q be given.

Assume H1.

We will prove PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q.

Apply orIL to the current goal.

An exact proof term for the current goal is H1.

∎