Let L and alpha be given.

Assume Ha.

Let p be given.

Assume H1: L alpha p.

We will prove ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe alpha p beta q.

We use alpha to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Ha.

We use p to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

Apply PNoLe_ref to the current goal.

∎