Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Assume H0:
∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3).
Apply unknownprop_e08a04d424da13101fe4a24b5b4e61037f5c9a4ddbf473297ae7bfacedd63b2c with
x0,
λ x3 . x1 x3,
0fc90.. x0 (λ x3 . x2 x3) leaving 2 subgoals.
Let x3 of type ι be given.
Apply unknownprop_d4dc73f3cbfe4c22363272ac418d035b8e77c49433b0870b96bee8fa9c46bfcf with
x0,
x2,
x3.
The subproof is completed by applying H1.
Apply exandE_i with
λ x4 . prim1 x4 x0,
λ x4 . ∃ x5 . and (prim1 x5 (x2 x4)) (x3 = aae7a.. x4 x5),
and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0) leaving 2 subgoals.
The subproof is completed by applying L2.
Let x4 of type ι be given.
Apply exandE_i with
λ x5 . prim1 x5 (x2 x4),
λ x5 . x3 = aae7a.. x4 x5,
and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x5 of type ι be given.
Assume H5:
prim1 x5 (x2 x4).
Apply andI with
cad8f.. x3,
prim1 (f482f.. x3 4a7ef..) x0 leaving 2 subgoals.
Apply H6 with
λ x6 x7 . cad8f.. x7.
The subproof is completed by applying unknownprop_74e7cf1e344053cc0ec428569910c022764085f38ffd3769b306f1021b002573 with x4, x5.
Apply H6 with
λ x6 x7 . prim1 (f482f.. x7 4a7ef..) x0.
Apply unknownprop_faec30ccee17d5393df69f9f5bea99ea0c13abcbefd6cdd0db4986d76425691f with
x4,
x5,
λ x6 x7 . prim1 x7 x0.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
x0,
x2,
x3,
λ x4 x5 . prim1 x5 (x1 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H0 with
x3.
The subproof is completed by applying H1.