Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: ∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0).

Assume H1: ∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3).

Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with e5b72.. (0fc90.. x0 (λ x3 . prim3 (x1 x3))), λ x3 . ∀ x4 . prim1 x4 x0 ⟶ prim1 (f482f.. x3 x4) (x1 x4), x2 leaving 2 subgoals.

Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with 0fc90.. x0 (λ x3 . prim3 (x1 x3)), x2.

Let x3 of type ι be given.

Assume H2: prim1 x3 x2.

Apply H0 with x3, prim1 x3 (0fc90.. x0 (λ x4 . prim3 (x1 x4))) leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: aae7a.. (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)) = x3.

Assume H4: prim1 (f482f.. x3 4a7ef..) x0.

Apply H3 with λ x4 x5 . prim1 x4 (0fc90.. x0 (λ x6 . prim3 (x1 x6))).

Apply unknownprop_1f27075d0cd8d16888a609d68ca6246fb2307839dccadd646f85ab18bdcaae8e with x0, λ x4 . prim3 (x1 x4), f482f.. x3 4a7ef.., f482f.. x3 (4ae4a.. 4a7ef..) leaving 2 subgoals.

The subproof is completed by applying H4.

Apply UnionI with x1 (f482f.. x3 4a7ef..), f482f.. x3 (4ae4a.. 4a7ef..), f482f.. x2 (f482f.. x3 4a7ef..) leaving 2 subgoals.

Apply unknownprop_5843a53f522dbf92d80ac36289685067f008fd2f46b9067d54fc3bf68053a1a3 with x2, f482f.. x3 4a7ef.., f482f.. x3 (4ae4a.. 4a7ef..).

Apply H3 with λ x4 x5 . prim1 x5 x2.

The subproof is completed by applying H2.

Apply H1 with f482f.. x3 4a7ef...

The subproof is completed by applying H4.

The subproof is completed by applying H1.

■

Proofgold Proof