ZeqReplaceBi1Zeq0Mul1 Show Code edit
## Substitution
##
## (<-> ph (z.= (z.* A [ B ] ] ] ) D))
## (z.= [ B ] [ C ] )
## (<-> ph (z.= (z.* A [ [ [ C ] ) D))
##
thm (ZeqReplaceBi1Zeq0Mul1 () (
replacee (<-> ph (z.= (z.* A B) D))
substitution (z.= B C))
(<-> ph (z.= (z.* A C) D))
replacee substitution
(z.= B C)
A z.muleq2i
(z.= (z.* A B) (z.* A C))
ZeqReplaceBi1Zeq0
(<-> ph (z.= (z.* A C) D))
)
edit