Let R and alpha be given.
Assume Ha.
Let p be given.
Assume H1: R alpha p.
We will
prove ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q alpha p.
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.