EqReplaceEq1Add1Add1 Show Code edit
## Substitution
##
## (= A (+ B (+ C [ D ] ] ] )))
## (= [ D ] [ A' ] )
## (= A (+ B (+ C [ [ [ A' ] )))
##
thm (EqReplaceEq1Add1Add1 () (
replacee (= A (+ B (+ C D)))
substitution (= D A'))
(= A (+ B (+ C A')))
replacee substitution
(= D A')
C addeq2i
(= (+ C D) (+ C A'))
EqReplaceEq1Add1
(= A (+ B (+ C A')))
)
edit