An exact proof term for the current goal is (λX : set ⇒ In_rec_i_G_f X (In_rec_i X) (F X In_rec_i) (In_rec_i_G_In_rec_i X) (In_rec_i_G_In_rec_i_d X)).