const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 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 SNoLev : set set const minus_SNo : set set term - = minus_SNo axiom minus_SNo_Lev: !x:set.SNo x -> SNoLev - x = SNoLev x axiom not_nonneg_abs_SNo: !x:set.~ Empty <= x -> abs_SNo x = - x axiom xm: !P:prop.P | ~ P claim !x:set.SNo x -> SNoLev (abs_SNo x) = SNoLev x