Let x0 of type ι be given.
Apply xm with
∃ x1 . and (prim1 x1 x0) (x0 = 4ae4a.. x1),
or (∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) x0) (∃ x1 . and (prim1 x1 x0) (x0 = 4ae4a.. x1)) leaving 2 subgoals.
Apply orIL with
∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) x0,
∃ x1 . and (prim1 x1 x0) (x0 = 4ae4a.. x1).
Let x1 of type ι be given.
Apply unknownprop_be250f85f3dffbb916064f41a6351d4768b4e417d7e89dc1e1bbd4f0f22c18a7 with
x0,
x1,
prim1 (4ae4a.. x1) x0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply FalseE with
prim1 (4ae4a.. x1) x0.
Apply H1.
Let x2 of type ο be given.
Apply H4 with
x1.
Apply andI with
prim1 x1 x0,
x0 = 4ae4a.. x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.