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