Let x0 of type ι be given.
Apply H0 with
∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (4ae4a.. x0) ⟶ fe4bb.. x1 x0.
Let x1 of type ι be given.
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_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with
x0,
e4431.. x1,
fe4bb.. x1 x0 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_3bb88212dd853920577537bc3ecbc5e3e2bf8309e1e59246b79ae30400fc333e with
x1,
x0.
Apply unknownprop_6987e7564cf46ad4d313ff96c864cc87566281cc7f9f5613cde1c6af34a43fdb with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
Apply dneg with
fe4bb.. x1 x0.
Apply ordinal_ind with
λ x2 . prim1 x2 x0 ⟶ prim1 x2 x1.
Let x2 of type ι be given.
Apply dneg with
prim1 x2 x1.
Apply H8.
Apply unknownprop_3bb88212dd853920577537bc3ecbc5e3e2bf8309e1e59246b79ae30400fc333e with
x1,
x0.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x2.
The subproof is completed by applying H9.
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with
x2.
The subproof is completed by applying H9.
Apply unknownprop_fb545b225a42993d98e0d062b6c9208b8321e87814f4e26de3418c134068c2c8 with
x1,
x2,
x0 leaving 5 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L13.
The subproof is completed by applying L5.
Apply unknownprop_e5e2df80485f871d64db3fb7f1a412399ce7964e3a578b5b796bab945938f5f4 with
x1,
x2 leaving 3 subgoals.
Apply L14 with
λ x3 x4 . prim1 x4 (e4431.. x1).
Apply H7 with
λ x3 x4 . prim1 x2 x4.
The subproof is completed by applying H11.
Apply L14 with
λ x3 x4 . SNoEq_ x4 x1 x2.
Let x3 of type ι be given.
Apply iffI with
prim1 x3 x1,
prim1 x3 x2 leaving 2 subgoals.
The subproof is completed by applying H15.
Apply H10 with
x3 leaving 2 subgoals.
The subproof is completed by applying H15.
Apply H1 with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H15.
Apply L14 with
λ x3 x4 . nIn x4 x1.
The subproof is completed by applying H12.
Apply unknownprop_397dcfaa62ddf41d498e7fd580ff4a854ed9ebd3c9ab727b2b23fe272ecb1aa4 with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H11.
Let x2 of type ι be given.
Apply L9 with
x2 leaving 2 subgoals.
Apply ordinal_Hered with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H10.
The subproof is completed by applying H10.
Claim L11: x1 = x0
Apply unknownprop_c3102c186c7aa1001a5c1b1b7ecab6b25bcd639e713104221ece8bf414726a69 with
x1,
x0 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
Apply L6 with
λ x2 x3 . e4431.. x1 = x3.
The subproof is completed by applying H7.
Apply H7 with
λ x2 x3 . SNoEq_ x3 x1 x0.
Let x2 of type ι be given.
Apply iffI with
prim1 x2 x1,
prim1 x2 x0 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply L10 with
x2.
The subproof is completed by applying H11.
Apply H8.
Apply L11 with
λ x2 x3 . fe4bb.. x3 x0.
The subproof is completed by applying unknownprop_f017f6ee910dd235f4bf08afbbbf148d42e1360d8b1094fb435baedbfe8b2ac8 with x0.