Let x0 of type ι be given.
Apply set_ext with
aae7a.. 4a7ef.. x0,
f6917.. x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_c7550417d862f27710857dc7f3a47fd61afe15d66581922367eb5c5641bfab12 with
4a7ef..,
x0,
x1,
prim1 x1 (f6917.. x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply exandE_i with
λ x2 . prim1 x2 4a7ef..,
λ x2 . x1 = f6917.. x2,
prim1 x1 (f6917.. x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply FalseE with
x1 = f6917.. x2 ⟶ prim1 x1 (f6917.. x0).
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x2.
The subproof is completed by applying H2.
Apply exandE_i with
λ x2 . prim1 x2 x0,
λ x2 . x1 = 09364.. x2,
prim1 x1 (f6917.. x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply H3 with
λ x3 x4 . prim1 x4 (f6917.. x0).
Apply unknownprop_cb49923233a17bfcdaaace11cf639914b23f1e115c13971fdab382102fec388a with
x0,
x2.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Apply exandE_i with
λ x2 . prim1 x2 x0,
λ x2 . x1 = 09364.. x2,
prim1 x1 (aae7a.. 4a7ef.. x0) leaving 2 subgoals.
Apply unknownprop_a63bdc277f1325cdd852a9c9272f39668f29a68974de510ddb75e64c4c429794 with
x0,
x1.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply H2 with
λ x3 x4 . prim1 x4 (aae7a.. 4a7ef.. x0).
Apply unknownprop_21bfd05a2dded69408d4a77ad07f3965317c49d7fa73834904d6def11389f597 with
4a7ef..,
x0,
x2.
The subproof is completed by applying H1.