const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const SNo : set prop 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 ordsucc : set set const Empty : set const minus_SNo : set set term - = minus_SNo const SNoR : set set const SNoS_ : set set const SNoLev : set set var x:set var y:set var z:set hyp SNo x hyp !w:set.w iIn SNoS_ (SNoLev x) -> w * ordsucc Empty = w hyp z iIn SNoR x hyp y = z * ordsucc Empty + x * Empty + - z * Empty hyp SNo z claim y = z -> y iIn SNoR x