theorem :: REWRITE3:1

canceled;