Generalize `mlRewrite` and `mlRewriteBy`

[berpeti]

These tactics should work for arbitrary contexts, not just simple ones. For example:

H : G |- a <---> b
__________________
G |- 
  foldr patt_imp l a ---> foldr patt_imp l b

This limitation comes from the following line in tactic heat:

 assert(heq1 : ($phi = (@emplace _ $pc $a))) 
         > [ abstract(
             (ltac1:(star |- simplify_emplace_2 star) (Ltac1.of_ident star_ident);
             reflexivity
             ))
           | ()
           ];

simplify_emplace_2 is not able to solve the asserted goal. One option would be to leave such goals to the user instead of failing.