const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLev : set set const If_i : prop set set set axiom SNo_rec2_G_prop: !P:set set (set set set) set.(!x:set.SNo x -> !y:set.SNo y -> !g:set set set.!h:set set set.(!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) -> P x y g = P x y h) -> !x:set.SNo x -> !g:set set set.!h:set set set.(!y:set.y iIn SNoS_ (SNoLev x) -> g y = h y) -> !y:set.SNo y -> !f:set set.!f2:set set.(!z:set.z iIn SNoS_ (SNoLev y) -> f z = f2 z) -> P x y (\z:set.\w:set.If_i (z = x) (f w) (g z w)) = P x y \z:set.\w:set.If_i (z = x) (f2 w) (h z w) var P:set set (set set set) set var x:set var g:set set set var y:set var f:set set var f2:set set hyp !z:set.SNo z -> !w:set.SNo w -> !h:set set set.!g2:set set set.(!u:set.u iIn SNoS_ (SNoLev z) -> !v:set.SNo v -> h u v = g2 u v) -> (!u:set.u iIn SNoS_ (SNoLev w) -> h z u = g2 z u) -> P z w h = P z w g2 hyp SNo x hyp SNo y hyp !z:set.z iIn SNoS_ (SNoLev y) -> f z = f2 z claim (!z:set.z iIn SNoS_ (SNoLev x) -> g z = g z) -> P x y (\z:set.\w:set.If_i (z = x) (f w) (g z w)) = P x y \z:set.\w:set.If_i (z = x) (f2 w) (g z w)