const ReplSep : set (set prop) (set set) set const Inj1 : set set const Unj : set set term proj1 = \x:set.ReplSep x (\y:set.?z:set.Inj1 z = y) Unj const In : set set prop term iIn = In infix iIn 2000 2000 axiom ReplSepI: !x:set.!p:set prop.!f:set set.!y:set.y iIn x -> p y -> f y iIn ReplSep x p f axiom Unj_Inj1_eq: !x:set.Unj (Inj1 x) = x const setsum : set set set const ordsucc : set set const Empty : set axiom Inj1_pair_1_eq: Inj1 = setsum (ordsucc Empty) claim !x:set.!y:set.setsum (ordsucc Empty) y iIn x -> y iIn proj1 x