EqReplaceImp1Eq0Add0 Show Code edit
## Substitution
##
## (-> ph (= (+ [ A ] ] ] C) D))
## (= [ A ] [ B ] )
## (-> ph (= (+ [ [ [ B ] C) D))
##
thm (EqReplaceImp1Eq0Add0 () (
replacee (-> ph (= (+ A C) D))
substitution (= A B))
(-> ph (= (+ B C) D))
replacee substitution
(= A B)
C addeq1i
(= (+ A C) (+ B C))
EqReplaceImp1Eq0
(-> ph (= (+ B C) D))
)
edit