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.
Apply H2 with
x1.
Apply andI with
ordinal x1,
∃ x4 : ι → ο . and (x0 x1 x4) (35b9b.. 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) (35b9b.. x1 x5 x1 x2) ⟶ x4.
Apply H3 with
x2.
Apply andI with
x0 x1 x2,
35b9b.. x1 x2 x1 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_ac07215c6ebe89023e9a4e8747fc5b9f09008a47b8850229ec563a36216227e7 with x1, x2.