Let x0 of type ι → (ι → ι → ι) → ι → ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι → ι be given.

Assume H0: ∀ x3 . prim1 x3 x1 ⟶ In_rec_G_ii x0 x3 (x2 x3).

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

Assume H1: ∀ x4 . ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5).

Apply H1 with x1, x2.

Let x4 of type ι be given.

Assume H2: prim1 x4 x1.

Apply H0 with x4, x3 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H1.

■

Proofgold Proof