const ordinal : set prop const SetAdjoin : set set set const Sing : set set const ordsucc : set set const Empty : set const Subq : set set prop axiom tagged_eqE_Subq: !x:set.!y:set.ordinal x -> SetAdjoin x (Sing (ordsucc Empty)) = SetAdjoin y (Sing (ordsucc Empty)) -> Subq x y axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !x:set.!y:set.ordinal x -> ordinal y -> SetAdjoin x (Sing (ordsucc Empty)) = SetAdjoin y (Sing (ordsucc Empty)) -> x = y