Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: prim0 (prim0 (prim1 (λ x3 . prim1 (λ x4 . prim0 (prim0 (prim0 x4 x3) (prim0 x3 x4)) (prim0 (prim0 x4 x4) (prim0 x3 x3))))) x1) x2 = prim0 (prim1 (λ x3 . prim1 (λ x4 . prim0 (prim0 (prim0 x4 x3) (prim0 x3 x4)) (prim0 (prim0 x4 x4) (prim0 x3 x3))))) x0.

Apply unknownprop_47684d77daf9976982fef9cd65f54cb0f256a9046ee087c4a3bf5f6bf45def6c with x0, x1, x2.

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

The subproof is completed by applying H0 with λ x4 x5 . x3 x5 x4.

■

Proofgold Proof