Let L and α be given.

Assume Ha.

Let p be given.

Assume H1: L α p.

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

We use α 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.

∎