Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: nIn x2 x0.

Apply unknownprop_fa66e3d1737b2c05fa4008399b4c740ee88bf9334c6b435957b41684dfedfe51 with f482f.. (0fc90.. x0 (λ x3 . x1 x3)) x2.

Let x3 of type ι be given.

Assume H1: prim1 x3 (f482f.. (0fc90.. x0 (λ x4 . x1 x4)) x2).

Claim L2: prim1 (aae7a.. x2 x3) (0fc90.. x0 (λ x4 . x1 x4))

Apply unknownprop_94a9448d53fe41e2f423017518d13b5ed4aaa7ee3f113a3a8a767ea0e11959dd with 0fc90.. x0 (λ x4 . x1 x4), x2, x3.

The subproof is completed by applying H1.

Claim L3: prim1 x2 x0

Apply unknownprop_65b697ce826092f2cc43df41585fc87a51cbb42f47ea078876e421084559202e with x0, x1, x2, x3.

The subproof is completed by applying L2.

Apply H0.

The subproof is completed by applying L3.

■

Proofgold Proof