Let x0 of type ι be given.
Apply and3I with
∀ x1 . prim1 x1 x0 ⟶ 80242.. x1,
∀ x1 . prim1 x1 4a7ef.. ⟶ 80242.. x1,
∀ x1 . prim1 x1 x0 ⟶ ∀ x2 . prim1 x2 4a7ef.. ⟶ 099f3.. x1 x2 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply FalseE with
80242.. x1.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply FalseE with
099f3.. x1 x2.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x2.
The subproof is completed by applying H2.