const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const SNoR : set set const SNoS_ : set set const SNoLev : set set axiom SNoR_SNoS_: !x:set.Subq (SNoR x) (SNoS_ (SNoLev x)) const Repl : set (set set) set axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P axiom ReplI: !x:set.!f:set set.!y:set.y iIn x -> f y iIn Repl x f axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y const binunion : set set set const Empty : set axiom binunion_idl: !x:set.binunion Empty x = x axiom Repl_Empty: !f:set set.Repl Empty f = Empty axiom SNoR_0: SNoR Empty = Empty const SNo : set prop const add_SNo : set set set term + = add_SNo infix + 2281 2280 const SNoL : set set const SNoCut : set set set lemma !x:set.SNo x -> (!y:set.y iIn SNoS_ (SNoLev x) -> Empty + y = y) -> binunion (Repl (SNoL Empty) \y:set.y + x) (Repl (SNoL x) (add_SNo Empty)) = SNoL x -> binunion (Repl (SNoR Empty) \y:set.y + x) (Repl (SNoR x) (add_SNo Empty)) = SNoR x -> SNoCut (binunion (Repl (SNoL Empty) \y:set.y + x) (Repl (SNoL x) (add_SNo Empty))) (binunion (Repl (SNoR Empty) \y:set.y + x) (Repl (SNoR x) (add_SNo Empty))) = x var x:set hyp SNo x hyp !y:set.y iIn SNoS_ (SNoLev x) -> Empty + y = y claim binunion (Repl (SNoL Empty) \y:set.y + x) (Repl (SNoL x) (add_SNo Empty)) = SNoL x -> SNoCut (binunion (Repl (SNoL Empty) \y:set.y + x) (Repl (SNoL x) (add_SNo Empty))) (binunion (Repl (SNoR Empty) \y:set.y + x) (Repl (SNoR x) (add_SNo Empty))) = x