Apply In_ind to the current goal.
Let X be given.
Assume IH: ∀x ∈ X, In_rec_G_iii x (In_rec_iii x).
We will prove In_rec_G_iii X (In_rec_iii X).
We will prove In_rec_G_iii X (Descr_iii (In_rec_G_iii X)).
Apply (Descr_iii_prop (In_rec_G_iii X)) to the current goal.
We use (F X In_rec_iii) to witness the existential quantifier.
We will prove In_rec_G_iii X (F X In_rec_iii).
An exact proof term for the current goal is (In_rec_G_iii_c X In_rec_iii IH).
An exact proof term for the current goal is In_rec_G_iii_f X.
∎