const Sep : set (set prop) set const SNoS_ : set set const SNoLev : set set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 term SNoR = \x:set.Sep (SNoS_ (SNoLev x)) (SNoLt x) const Subq : set set prop axiom Sep_Subq: !x:set.!p:set prop.Subq (Sep x p) x claim !x:set.Subq (SNoR x) (SNoS_ (SNoLev x))