Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Assume H1: x0 x1 x2.
Let x3 of type ο be given.
Assume H2:
∀ x4 . and (ordinal x4) (∃ x5 : ι → ο . and (x0 x4 x5) (PNoLe x4 x5 x1 x2)) ⟶ x3.
Apply H2 with
x1.
Apply andI with
ordinal x1,
∃ x4 : ι → ο . and (x0 x1 x4) (PNoLe x1 x4 x1 x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ο be given.
Assume H3:
∀ x5 : ι → ο . and (x0 x1 x5) (PNoLe x1 x5 x1 x2) ⟶ x4.
Apply H3 with
x2.
Apply andI with
x0 x1 x2,
PNoLe x1 x2 x1 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying PNoLe_ref with x1, x2.