const In : set set prop term iIn = In infix iIn 2000 2000 const In_rec_i_G : (set (set set) set) set set prop const In_rec_i : (set (set set) set) set set axiom In_rec_i_G_In_rec_i: !P:set (set set) set.(!x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> P x f = P x f2) -> !x:set.In_rec_i_G P x (In_rec_i P x) axiom In_rec_i_G_In_rec_i_d: !P:set (set set) set.(!x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> P x f = P x f2) -> !x:set.In_rec_i_G P x (P x (In_rec_i P)) axiom In_rec_i_G_f: !P:set (set set) set.(!x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> P x f = P x f2) -> !x:set.!y:set.!z:set.In_rec_i_G P x y -> In_rec_i_G P x z -> y = z claim !P:set (set set) set.(!x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> P x f = P x f2) -> !x:set.In_rec_i P x = P x (In_rec_i P)