An exact proof term for the current goal is (λX : set ⇒ In_rec_G_iii_f X (In_rec_iii X) (F X In_rec_iii) (In_rec_G_iii_In_rec_iii X) (In_rec_G_iii_In_rec_iii_d X)).