const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f const In : set set prop term iIn = In infix iIn 2000 2000 term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) term nIn = \x:set.\y:set.~ x iIn y term SNoEq_ = \x:set.\y:set.\z:set.PNoEq_ x (\w:set.w iIn y) \w:set.w iIn z const SNo : set prop const SNoLev : set set const binintersect : set set set const SNoElts_ : set set axiom restr_SNoEq: !x:set.SNo x -> !y:set.y iIn SNoLev x -> SNoEq_ y (binintersect x (SNoElts_ y)) x axiom iff_sym: !P:prop.!Q:prop.(P <-> Q) -> (Q <-> P) axiom iff_trans: !P:prop.!Q:prop.!R:prop.(P <-> Q) -> (Q <-> R) -> (P <-> R) axiom FalseE: ~ False axiom iffI: !P:prop.!Q:prop.(P -> Q) -> (Q -> P) -> (P <-> Q) const ordsucc : set set axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x axiom SNo_eq: !x:set.!y:set.SNo x -> SNo y -> SNoLev x = SNoLev y -> SNoEq_ (SNoLev x) x y -> x = y const add_SNo : set set set term + = add_SNo infix + 2281 2280 const exp_SNo_nat : set set set const Empty : set const Sep : set (set prop) set const SNoS_ : set set const omega : set var x:set var f:set set var y:set var z:set hyp SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp !w:set.w iIn Sep (SNoS_ omega) (\u:set.SNoLev u = x) -> !u:set.u iIn Sep (SNoS_ omega) (\v:set.SNoLev v = x) -> f w = f u -> w = u hyp SNo y hyp SNoLev y = ordsucc x hyp binintersect y (SNoElts_ x) iIn Sep (SNoS_ omega) \w:set.SNoLev w = x hyp SNo (f (binintersect y (SNoElts_ x))) hyp SNo z hyp SNoLev z = ordsucc x hyp binintersect z (SNoElts_ x) iIn Sep (SNoS_ omega) \w:set.SNoLev w = x hyp SNo (f (binintersect z (SNoElts_ x))) hyp x iIn SNoLev y hyp x iIn SNoLev z hyp nIn x y hyp nIn x z hyp exp_SNo_nat (ordsucc (ordsucc Empty)) x + f (binintersect y (SNoElts_ x)) = exp_SNo_nat (ordsucc (ordsucc Empty)) x + f (binintersect z (SNoElts_ x)) claim binintersect y (SNoElts_ x) = binintersect z (SNoElts_ x) -> y = z