Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
x0,
λ x2 . (λ x3 . 15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x2,
(λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1,
prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Claim L5: x1 = x2
Apply unknownprop_e5b694101db633e1cb8f386839a36365a4221afba1aae387465fef7a38c126b7 with
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply ordinal_Hered with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply L5 with
λ x3 x4 . prim1 x4 x0.
The subproof is completed by applying H3.