Let x0 of type ι be given.
Let x1 of type ι be given.
Apply ordinal_In_Or_Subq with
x0,
x1,
prim1 x0 (4ae4a.. x1) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_4c4b27a97d7f3e81d4abb7629b850d6c55c186f55f30e3dfae132a3ddf1e0a30 with
x1,
x0.
The subproof is completed by applying H3.
Claim L4: x0 = x1
Apply set_ext with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply L4 with
λ x2 x3 . prim1 x3 (4ae4a.. x1).
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x1.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_a01a97b657898ff9d288e2af990470253bea0ca012cb491bf0a3063b2cc95ddb with
x1,
x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.
Apply L5 with
λ x2 x3 . prim1 x3 (4ae4a.. x1).
The subproof is completed by applying L3.