addeq2d Show Code edit
## Equality over Addition
thm (addeq2d ()
(h (-> ph (= A B)))
(-> ph (= (+ C A) (+ C B)))
h A B C addeq2 syl
(-> ph (= (+ C A) (+ C B)))
)
edit