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