Let X and Y be given.

Assume H1: In_rec_G_iii X Y.

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

Apply (H1 R) to the current goal.

We will prove ∀Z : set, ∀g : set → (set → 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 → set → set), (∀x ∈ z, In_rec_G_iii x (f x)) ∧ g z = F z f.

We will prove ∃f : set → (set → set → set), (∀x ∈ Z, In_rec_G_iii 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_iiii (λf ⇒ ∀x ∈ z, In_rec_G_iii x (f x)) (λf ⇒ g z = F z f) (IH z H2)) to the current goal.

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

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

Assume H4: g z = F z f.

We will prove In_rec_G_iii z (g z).

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

We will prove In_rec_G_iii z (F z f).

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

An exact proof term for the current goal is (λq H ⇒ H).

∎