Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_e96b280cab6654d7b29280b5ca69e751c7596719bb8b0145df6b081d02028fee with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply ordinal_In_Or_Subq with
4ae4a.. x1,
x0,
prim1 (4ae4a.. x1) (4ae4a.. x0) leaving 4 subgoals.
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
x1.
Apply ordinal_Hered with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_4c4b27a97d7f3e81d4abb7629b850d6c55c186f55f30e3dfae132a3ddf1e0a30 with
x0,
4ae4a.. x1.
The subproof is completed by applying H3.
Apply set_ext with
4ae4a.. x1,
x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H3.
Apply L4 with
λ x2 x3 . prim1 x3 (4ae4a.. x0).
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x0.