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.

Let x3 of type ι be given.

Assume H1: prim1 x3 (e5b72.. x0).

Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with x1, 94f9e.. x3 (λ x4 . x2 x4).

Let x4 of type ι be given.

Assume H2: prim1 x4 (94f9e.. x3 (λ x5 . x2 x5)).

Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x3, x2, x4, prim1 x4 x1 leaving 2 subgoals.

The subproof is completed by applying H2.

Let x5 of type ι be given.

Assume H3: prim1 x5 x3.

Assume H4: x4 = x2 x5.

Apply H4 with λ x6 x7 . prim1 x7 x1.

Apply H0 with x5.

Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with x0, x3, x5 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

■

Proofgold Proof