Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, In_rec_i_G x (In_rec_i x).

We will prove In_rec_i_G X (In_rec_i X).

We will prove In_rec_i_G X (Eps_i (In_rec_i_G X)).

Apply (Eps_i_ax (In_rec_i_G X) (F X In_rec_i)) to the current goal.

We will prove In_rec_i_G X (F X In_rec_i).

An exact proof term for the current goal is (In_rec_i_G_c X In_rec_i IH).

∎