UnorderedPair-sub Show Code edit
thm (UnorderedPair-sub () () (→ (= C D) (↔ (∨ (= C A) (= C B)) (∨ (= D A) (= D B))))
C D A EqualityBuilderRR
(→ (= C D) (↔ (= C A) (= D A)))
C D B EqualityBuilderRR
(→ (= C D) (↔ (= C B) (= D B)))
buildDisjunctionInConsequent
(→ (= C D) (↔ (∨ (= C A) (= C B)) (∨ (= D A) (= D B))))
)
edit