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 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 z -> (?f:set set.(!w:set.w iIn x -> In_rec_i_G P w (f w)) & y = P x f) -> (?f:set set.(!w:set.w iIn x -> In_rec_i_G P w (f w)) & z = P x f) -> y = z var P:set (set set) set var x:set var y:set var z:set hyp !w:set.!f:set set.!f2:set set.(!u:set.u iIn w -> f u = f2 u) -> P w f = P w f2 hyp !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 hyp In_rec_i_G P x y hyp In_rec_i_G P x z claim (?f:set set.(!w:set.w iIn x -> In_rec_i_G P w (f w)) & y = P x f) -> y = z