ZeqReplaceBi1An0Zeq0 Show Code edit
## Substitution
##
## (<-> ph (/\ (z.= [ A ] ] ] C) ps))
## (z.= [ A ] [ B ] )
## (<-> ph (/\ (z.= [ [ [ B ] C) ps))
##
thm (ZeqReplaceBi1An0Zeq0 () (
replacee (<-> ph (/\ (z.= A C) ps))
substitution (z.= A B))
(<-> ph (/\ (z.= B C) ps))
replacee substitution
(z.= A B)
C z.eqeq1i
(<-> (z.= A C) (z.= B C))
BiReplaceBi1An0
(<-> ph (/\ (z.= B C) ps))
)
edit