Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
x1,
λ x2 . (λ x3 . 15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x2,
x0,
False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply unknownprop_81d5bf525fa56ced1f50f507419c213d2f5baf8a9bd690d88066a9046e094314 with
x2.
Apply H3 with
λ x3 x4 . ordinal x3.
The subproof is completed by applying H0.