const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term TransSet = \x:set.!y:set.y iIn x -> Subq y x term ordinal = \x:set.TransSet x & !y:set.y iIn x -> TransSet y const In_rec_ii : (set (set set set) set set) set set set const If_ii : prop (set set) (set set) set set const If_i : prop set set set const SNoS_ : set set const ordsucc : set set const SNoLev : set set const Eps_i : (set prop) set term SNo_rec_i = \P:set (set set) set.\x:set.In_rec_ii (\y:set.\g:set set set.If_ii (ordinal y) (\z:set.If_i (z iIn SNoS_ (ordsucc y)) (P z \w:set.g (SNoLev w) w) (Eps_i \w:set.True)) \z:set.Eps_i \w:set.True) (SNoLev x) x term nIn = \x:set.\y:set.~ x iIn y var x:set var g:set set set var h:set set set var y:set var z:set hyp !w:set.w iIn x -> g w = h w hyp ordinal x hyp SNoLev y iIn ordsucc x hyp SNoLev z iIn SNoLev y claim SNoLev z iIn x -> g (SNoLev z) z = h (SNoLev z) z