Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply L1 with
and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4).
Let x5 of type ι be given.
Apply H2 with
and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4).
Apply H4 with
and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4).
Let x6 of type ι be given.
Apply H5 with
and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4).
Assume H6:
prim1 x6 (x1 x5).
Apply H7 with
and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4).
Assume H9: x2 x5 x6.
Apply unknownprop_1d98a2dc54199f22cd9592e66e7c1294600579525b000a5cf24e785ed12e9f6a with
x3,
x4,
x5,
x6,
and (and (prim1 x3 x0) (prim1 ... ...)) ... leaving 2 subgoals.