const SNo_rec2 : (set set (set set set) set) set set set const SNoCut : set set set const binunion : set set set const Repl : set (set set) set const SNoL : set set const SNoR : set set term add_SNo = SNo_rec2 \x:set.\y:set.\g:set set set.SNoCut (binunion (Repl (SNoL x) \z:set.g z y) (Repl (SNoL y) (g x))) (binunion (Repl (SNoR x) \z:set.g z y) (Repl (SNoR y) (g x))) term + = add_SNo infix + 2281 2280 const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLev : set set axiom SNoR_SNoS: !x:set.SNo x -> !y:set.y iIn SNoR x -> y iIn SNoS_ (SNoLev x) axiom ReplEq_ext: !x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> Repl x f = Repl x f2 lemma !x:set.!y:set.!g:set set set.!h:set set set.SNo x -> SNo y -> (!z:set.z iIn SNoS_ (SNoLev x) -> !w:set.SNo w -> g z w = h z w) -> (!z:set.z iIn SNoS_ (SNoLev y) -> g x z = h x z) -> Repl (SNoL x) (\z:set.g z y) = Repl (SNoL x) (\z:set.h z y) -> Repl (SNoL y) (g x) = Repl (SNoL y) (h x) -> Repl (SNoR x) (\z:set.g z y) = Repl (SNoR x) (\z:set.h z y) -> SNoCut (binunion (Repl (SNoL x) \z:set.g z y) (Repl (SNoL y) (g x))) (binunion (Repl (SNoR x) \z:set.g z y) (Repl (SNoR y) (g x))) = SNoCut (binunion (Repl (SNoL x) \z:set.h z y) (Repl (SNoL y) (h x))) (binunion (Repl (SNoR x) \z:set.h z y) (Repl (SNoR y) (h x))) var x:set var y:set var g:set set set var h:set set set hyp SNo x hyp SNo y hyp !z:set.z iIn SNoS_ (SNoLev x) -> !w:set.SNo w -> g z w = h z w hyp !z:set.z iIn SNoS_ (SNoLev y) -> g x z = h x z hyp Repl (SNoL x) (\z:set.g z y) = Repl (SNoL x) \z:set.h z y claim Repl (SNoL y) (g x) = Repl (SNoL y) (h x) -> SNoCut (binunion (Repl (SNoL x) \z:set.g z y) (Repl (SNoL y) (g x))) (binunion (Repl (SNoR x) \z:set.g z y) (Repl (SNoR y) (g x))) = SNoCut (binunion (Repl (SNoL x) \z:set.h z y) (Repl (SNoL y) (h x))) (binunion (Repl (SNoR x) \z:set.h z y) (Repl (SNoR y) (h x)))