Let X and Y be given.

Assume H1: In_rec_i_G X Y.

Set R to be the term (λX : set ⇒ λY : set ⇒ ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Y = F X f).

Apply (H1 R) to the current goal.

We will prove ∀Z : set, ∀g : set → set, (∀z ∈ Z, R z (g z)) → R Z (F Z g).

Let Z and g be given.

Assume IH: ∀z ∈ Z, ∃f : set → set, (∀x ∈ z, In_rec_i_G x (f x)) ∧ g z = F z f.

We will prove ∃f : set → set, (∀x ∈ Z, In_rec_i_G x (f x)) ∧ F Z g = F Z f.

We use g to witness the existential quantifier.

Apply andI to the current goal.

Let z be given.

Assume H2: z ∈ Z.

Apply (exandE_ii (λf ⇒ ∀x ∈ z, In_rec_i_G x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.

Let f of type set → set be given.

Assume H3: ∀x ∈ z, In_rec_i_G x (f x).

Assume H4: g z = F z f.

We will prove In_rec_i_G z (g z).

rewrite the current goal using H4 (from left to right).

We will prove In_rec_i_G z (F z f).

An exact proof term for the current goal is (In_rec_i_G_c z f H3).

Use reflexivity.

∎