avoid using rewrite_all because it is reserved in coq trunk