const ordinal : set prop const SNo_ : set set prop term SNo = \x:set.?y:set.ordinal y & SNo_ y x const PSNo : set (set prop) set const SNoLev : set set lemma !x:set.!p:set prop.ordinal x -> SNo_ x (PSNo x p) -> SNo (PSNo x p) -> SNoLev (PSNo x p) = x var x:set var p:set prop hyp ordinal x claim SNo_ x (PSNo x p) -> SNoLev (PSNo x p) = x