An exact proof term for the current goal is (λX : set ⇒ In_rec_G_ii_f X (In_rec_ii X) (F X In_rec_ii) (In_rec_G_ii_In_rec_ii X) (In_rec_G_ii_In_rec_ii_d X)).