const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoLe_ref: !x:set.x <= x const Empty : set const abs_SNo : set set axiom nonneg_abs_SNo: !x:set.Empty <= x -> abs_SNo x = x const SNo : set prop const add_SNo : set set set term + = add_SNo infix + 2281 2280 var x:set var y:set hyp SNo x hyp SNo y hyp Empty <= x hyp Empty <= y claim Empty <= x + y -> abs_SNo (x + y) <= x + y