Let alpha, p and q be given.

Assume H1.

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

Apply orIR to the current goal.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is H1.

∎