const In : set set prop term iIn = In infix iIn 2000 2000 term In_rec_i_G = \P:set (set set) set.\x:set.\y:set.!r:set set prop.(!z:set.!f:set set.(!w:set.w iIn z -> r w (f w)) -> r z (P z f)) -> r x y axiom In_rec_i_G_c: !P:set (set set) set.!x:set.!f:set set.(!y:set.y iIn x -> In_rec_i_G P y (f y)) -> In_rec_i_G P x (P x f) axiom exandE_ii: !P:(set set) prop.!Q:(set set) prop.(?f:set set.P f & Q f) -> !R:prop.(!f:set set.P f -> Q f -> R) -> R claim !P:set (set set) set.!x:set.!y:set.In_rec_i_G P x y -> ?f:set set.(!z:set.z iIn x -> In_rec_i_G P z (f z)) & y = P x f