const In_rec_i_G : (set (set set) set) set set prop const In : set set prop term iIn = In infix iIn 2000 2000 axiom In_rec_i_G_inv: !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 axiom In_ind: !p:set prop.(!x:set.(!y:set.y iIn x -> p y) -> p x) -> !x:set.p x lemma !P:set (set set) set.!x:set.!y:set.!z:set.(!w:set.!f:set set.!f2:set set.(!u:set.u iIn w -> f u = f2 u) -> P w f = P w f2) -> (!w:set.w iIn x -> !u:set.!v:set.In_rec_i_G P w u -> In_rec_i_G P w v -> u = v) -> In_rec_i_G P x y -> In_rec_i_G P x z -> (?f:set set.(!w:set.w iIn x -> In_rec_i_G P w (f w)) & y = P x f) -> 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.!y:set.!z:set.In_rec_i_G P x y -> In_rec_i_G P x z -> y = z