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