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.

Assume H0: ∀ x5 . prim1 x5 x2 ⟶ x3 x5 = x4 x5.

Apply xm with prim1 (prim3 x2) x2, (λ x5 . λ x6 : ι → ι . If_i (prim1 (prim3 x5) x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2 x3 = (λ x5 . λ x6 : ι → ι . If_i (prim1 (prim3 x5) x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2 x4 leaving 2 subgoals.

Assume H1: prim1 (prim3 x2) x2.

Apply H0 with prim3 x2, λ x5 x6 . If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) x6) x0 = If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 leaving 2 subgoals.

The subproof is completed by applying H1.

Let x5 of type ι → ι → ο be given.

Assume H2: x5 (If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0) (If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0).

The subproof is completed by applying H2.

Assume H1: nIn (prim3 x2) x2.

Claim L2: If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = x0

Apply If_i_0 with prim1 (prim3 x2) x2, x1 (prim3 x2) (x3 (prim3 x2)), x0.

The subproof is completed by applying H1.

Claim L3: If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 = x0

Apply If_i_0 with prim1 (prim3 x2) x2, x1 (prim3 x2) (x4 (prim3 x2)), x0.

The subproof is completed by applying H1.

Apply L3 with λ x5 x6 . If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = x6.

The subproof is completed by applying L2.

■

Proofgold Proof