Apply unknownprop_669df0da86db4f986bae532f93288cb46feb5b77310c7f6de7766507585de4c6 with λ x0 x1 : ι → ι . ∀ x2 x3 . prim1 (x0 x3) x2 ⟶ prim1 x3 (e76d4.. x2).

Let x0 of type ι be given.

Let x1 of type ι be given.

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

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

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

The subproof is completed by applying H0.

Let x2 of type ο be given.

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

Apply H1 with x1.

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

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

The subproof is completed by applying H2.

■

Proofgold Proof