Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: prim1 (aae7a.. x1 x2) x0.

Apply unknownprop_916f469d850241375b1e44b2c6308f0113078869ceee129c02712fae69c32a37 with x1, x2, λ x3 x4 . prim1 x3 (a4c2a.. x0 (λ x5 . ∃ x6 . x5 = aae7a.. x1 x6) (λ x5 . 22ca9.. x5)).

Apply unknownprop_9c424e90871cd9e3a05e6a3be208792c52ad17517e2db8ef40187e46ac0e9a6e with x0, λ x3 . ∃ x4 . x3 = aae7a.. x1 x4, 22ca9.., aae7a.. x1 x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x3 of type ο be given.

Assume H1: ∀ x4 . aae7a.. x1 x2 = aae7a.. x1 x4 ⟶ x3.

Apply H1 with x2.

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

Assume H2: x4 (aae7a.. x1 x2) (aae7a.. x1 x2).

The subproof is completed by applying H2.

■

Proofgold Proof