const If_i : prop set set set axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLev : set set const SNo : set prop var x:set var g:set set set var h:set set set var f:set set var f2:set set var y:set var z:set hyp SNo x hyp !w:set.w iIn SNoS_ (SNoLev x) -> g w = h w hyp y iIn SNoS_ (SNoLev x) claim y != x -> If_i (y = x) (f z) (g y z) = If_i (y = x) (f2 z) (h y z)