Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: ba9d8.. x1.

Let x2 of type ι be given.

Assume H1: aa8d2.. x1 x0 x2.

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

Assume H2: x3 4a7ef.. x0.

Assume H3: ∀ x4 . ba9d8.. x4 ⟶ ∀ x5 . x3 x4 x5 ⟶ x3 (4ae4a.. x4) (prim3 x5).

Apply H3 with x1, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply H1 with x3 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

■

Proofgold Proof