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 claim abs_SNo Empty = Empty