const binunion : set set set const Repl : set (set set) set const SetAdjoin : set set set const Sing : set set const ordsucc : set set const Empty : set term SNo_pair = \x:set.\y:set.binunion x (Repl y \z:set.SetAdjoin z (Sing (ordsucc (ordsucc Empty)))) axiom binunion_idr: !x:set.binunion x Empty = x axiom Repl_Empty: !f:set set.Repl Empty f = Empty claim !x:set.SNo_pair x Empty = x