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 minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - 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 -> SNo (abs_SNo x)