const SNo_rec_i : (set (set set) set) set set const SNoCut : set set set const Repl : set (set set) set const SNoR : set set const SNoL : set set term minus_SNo = SNo_rec_i \x:set.\f:set set.SNoCut (Repl (SNoR x) f) (Repl (SNoL x) f) term - = minus_SNo const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLev : set set axiom SNoR_SNoS: !x:set.SNo x -> !y:set.y iIn SNoR x -> y iIn SNoS_ (SNoLev x) axiom ReplEq_ext: !x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> Repl x f = Repl x f2 lemma (!x:set.SNo x -> !f:set set.!f2:set set.(!y:set.y iIn SNoS_ (SNoLev x) -> f y = f2 y) -> SNoCut (Repl (SNoR x) f) (Repl (SNoL x) f) = SNoCut (Repl (SNoR x) f2) (Repl (SNoL x) f2)) -> !x:set.SNo x -> SNo_rec_i (\y:set.\f:set set.SNoCut (Repl (SNoR y) f) (Repl (SNoL y) f)) x = SNoCut (Repl (SNoR x) (SNo_rec_i \y:set.\f:set set.SNoCut (Repl (SNoR y) f) (Repl (SNoL y) f))) (Repl (SNoL x) (SNo_rec_i \y:set.\f:set set.SNoCut (Repl (SNoR y) f) (Repl (SNoL y) f))) lemma !x:set.!f:set set.!f2:set set.SNo x -> (!y:set.y iIn SNoS_ (SNoLev x) -> f y = f2 y) -> Repl (SNoR x) f = Repl (SNoR x) f2 -> SNoCut (Repl (SNoR x) f) (Repl (SNoL x) f) = SNoCut (Repl (SNoR x) f2) (Repl (SNoL x) f2) claim !x:set.SNo x -> - x = SNoCut (Repl (SNoR x) \y:set.- y) (Repl (SNoL x) \y:set.- y)