Apply In_ind to the current goal.
Let X be given.
Assume IH: ∀x ∈ X, In_rec_G_ii x (In_rec_ii x).
We will prove In_rec_G_ii X (In_rec_ii X).
We will prove In_rec_G_ii X (Descr_ii (In_rec_G_ii X)).
Apply (Descr_ii_prop (In_rec_G_ii X)) to the current goal.
We use (F X In_rec_ii) to witness the existential quantifier.
We will prove In_rec_G_ii X (F X In_rec_ii).
An exact proof term for the current goal is (In_rec_G_ii_c X In_rec_ii IH).
An exact proof term for the current goal is In_rec_G_ii_f X.
∎