SingletonAsUnorderedPair Show Code edit
defthm (SingletonAsUnorderedPair object (singleton A) () ()
(= (singleton A) (unorderedPair A A))
(unorderedPair A A) EqualityReflexivity
(= (unorderedPair A A) (unorderedPair A A))
)
edit