Let X and R be given.

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

Apply (H1 X In_rec_iii) to the current goal.

Let x be given.

Assume _.

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

∎