Let X of type set be given.

Let f of type set → set be given.

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

We will prove In_rec_i_G X (F X f).

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

Assume H2: ∀X : set, ∀f : 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).

∎