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 Empty : set axiom EmptyE: !x:set.nIn x Empty axiom FalseE: ~ False const SNoR : set set axiom SNoR_0: SNoR Empty = Empty const SNoL : set set axiom SNoL_0: SNoL Empty = Empty axiom Empty_Subq_eq: !x:set.Subq x Empty -> x = Empty 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 const SNoCut : set set set lemma !x:set.!y:set.!z:set.(!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) -> y = Empty -> z = Empty -> SNoCut y z = Empty var x:set var y:set var z:set hyp !w:set.w iIn y -> !P:prop.(!u:set.u iIn SNoL x -> !v:set.v iIn SNoL Empty -> w = u * Empty + x * v + - u * v -> P) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoR Empty -> w = u * Empty + x * v + - u * v -> P) -> P 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 claim y = Empty -> SNoCut y z = Empty