const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const SNoCut : set set set const Empty : set axiom SNoCut_0_0: SNoCut Empty Empty = Empty const SNoL : set set const SNoR : set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const minus_SNo : set set term - = minus_SNo var x:set var y:set var z:set hyp !w:set.w iIn z -> !P:prop.(!u:set.u iIn SNoL x -> !v:set.v iIn SNoR Empty -> w = u * Empty + x * v + - u * v -> P) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoL Empty -> w = u * Empty + x * v + - u * v -> P) -> P hyp y = Empty claim z = Empty -> SNoCut y z = Empty