Let X of type set be given.

Let f of type set → (set → set) be given.

Assume H1: ∀x ∈ X, In_rec_G_ii x (f x).

We will prove In_rec_G_ii X (F X f).

Let R of type set → (set → set) → prop be given.

Assume H2: ∀X : set, ∀f : set → (set → set), (∀x ∈ X, R x (f x)) → R X (F X f).

We will prove R X (F X f).

Apply (H2 X f) to the current goal.

We will prove ∀x ∈ X, R x (f x).

Let x of type set be given.

Assume H3: x ∈ X.

We will prove R x (f x).

An exact proof term for the current goal is (H1 x H3 R H2).

∎