Let x0 of type ι be given.
Apply andI with
Subq x0 (472ec.. x0),
∀ x1 . prim1 x1 x0 ⟶ exactly1of2 (prim1 ((λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) x0) (prim1 x1 x0) leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with
x0,
94f9e.. x0 (λ x2 . (λ x3 . 15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x2),
x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply exactly1of2_I2 with
prim1 ((λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) x0,
prim1 x1 x0 leaving 2 subgoals.
Apply unknownprop_81d5bf525fa56ced1f50f507419c213d2f5baf8a9bd690d88066a9046e094314 with
x1.
Apply ordinal_Hered with
x0,
(λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.