Apply unknownprop_48f8d4859b6b78ba3bbfab79f28064a8eb2fee8b3008bbf7332b70f58b78e189 with λ x0 x1 : ι → ι . ∀ x2 x3 . prim1 (x0 x3) x2 ⟶ prim1 x3 (22ca9.. x2).

Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: prim1 (09364.. x1) x0.

Apply unknownprop_220466dabb9c90c9b087796465f1368ac3c1e9d1ef55643ebed4c27316fb8803 with x1, λ x2 x3 . prim1 x2 (a4c2a.. x0 (λ x4 . ∃ x5 . 09364.. x5 = x4) (λ x4 . 158d3.. x4)).

Apply unknownprop_9c424e90871cd9e3a05e6a3be208792c52ad17517e2db8ef40187e46ac0e9a6e with x0, λ x2 . ∃ x3 . 09364.. x3 = x2, 158d3.., 09364.. x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x2 of type ο be given.

Assume H1: ∀ x3 . 09364.. x3 = 09364.. x1 ⟶ x2.

Apply H1 with x1.

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

Assume H2: x3 (09364.. x1) (09364.. x1).

The subproof is completed by applying H2.

■

Proofgold Proof