Apply unknownprop_85336ee07ace71a942dc508d3b8c851d9d6bb88511443b7dafbf11b71c263f4d with
λ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 (4ae4a.. x0) ⟶ prim1 (x1 x2) x0) ⟶ not (∀ x2 . prim1 x2 (4ae4a.. x0) ⟶ ∀ x3 . prim1 x3 (4ae4a.. x0) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) leaving 2 subgoals.
Let x0 of type ι → ι be given.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x0 4a7ef..,
not (∀ x1 . prim1 x1 (4ae4a.. 4a7ef..) ⟶ ∀ x2 . prim1 x2 (4ae4a.. 4a7ef..) ⟶ x0 x1 = x0 x2 ⟶ x1 = x2).
Apply H0 with
4a7ef...
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.
Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Apply xm with
∃ x2 . and (prim1 x2 (4ae4a.. (4ae4a.. x0))) (x1 x2 = x0),
False leaving 2 subgoals.
Apply H4 with
False.
Let x2 of type ι be given.
Apply H5 with
False.
Assume H7: x1 x2 = x0.
Apply H1 with
λ x3 . If_i (Subq x2 x3) (x1 (4ae4a.. x3)) (x1 x3) leaving 2 subgoals.
Let x3 of type ι be given.
Apply xm with
Subq x2 x3,
prim1 ((λ x4 . If_i (Subq x2 x4) (x1 (4ae4a.. x4)) (x1 x4)) x3) x0 leaving 2 subgoals.
Apply If_i_1 with
Subq x2 x3,
x1 (4ae4a.. x3),
x1 x3,
λ x4 x5 . prim1 x5 x0 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with
x0,
x1 (4ae4a.. x3),
prim1 (x1 (4ae4a.. x3)) x0 leaving 3 subgoals.
Apply H2 with
4ae4a.. x3.
The subproof is completed by applying L10.
The subproof is completed by applying H11.
Apply FalseE with
prim1 (x1 (4ae4a.. x3)) x0.
Apply In_irref with
x3.
Apply L12 with
λ x4 x5 . prim1 ... ....
Apply H9 with
x3.
The subproof is completed by applying L13.