Let X and R be given.

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

Apply (H1 X In_rec_i) to the current goal.

Let x be given.

Assume _.

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

∎