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 In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLev : set set const SNo : set prop var x:set var f:set set var f2:set set hyp SNo x hyp !y:set.y iIn SNoS_ (SNoLev x) -> f y = f2 y hyp Repl (SNoR x) f = Repl (SNoR x) f2 claim Repl (SNoL x) f = Repl (SNoL x) f2 -> SNoCut (Repl (SNoR x) f) (Repl (SNoL x) f) = SNoCut (Repl (SNoR x) f2) (Repl (SNoL x) f2)