const SNo : set prop const SNo_extend0 : set set axiom SNo_extend0_SNo: !x:set.SNo x -> SNo (SNo_extend0 x) const binintersect : set set set const SNoElts_ : set set const SNoLev : set set lemma !x:set.SNo x -> SNo (SNo_extend0 x) -> x = binintersect (SNo_extend0 x) (SNoElts_ (SNoLev x)) claim !x:set.SNo x -> x = binintersect (SNo_extend0 x) (SNoElts_ (SNoLev x))