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: prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2).

Claim L1: and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4)

Apply unknownprop_0d0b4194fab77127c359e0ea4da0082fbc6cb63a1f3d2bf9d40caed8dc882254 with x0, x1, x2, x3, x4.

The subproof is completed by applying H0.

Apply L1 with prim1 x4 (x1 x3).

Assume H2: and (prim1 x3 x0) (prim1 x4 (x1 x3)).

Assume H3: x2 x3 x4.

Apply H2 with prim1 x4 (x1 x3).

Assume H4: prim1 x3 x0.

Assume H5: prim1 x4 (x1 x3).

The subproof is completed by applying H5.

■

Proofgold Proof