rewrite
add ModusPonens