Merge pull request #224 from herbelin/master+adapt-coq-pr18591-simpl-…

…never-refolding

Adapt to Coq PR #18591: better refolding of List.app inducing "simpl never" now better respected

theories/StringRewriting/Reductions/MM2_ZERO_HALTING_to_SSTS01.v

@@ -603,7 +603,7 @@ Proof.
   elim: u s.
   - move=> [|y1 [|y2 s]].
     + rewrite ?app_nil_l. move=> <-. right. right. by exists [].
-    + move=> [] <- <- /=. right. by left.
+    + move=> []. rewrite [in [] ++ _]/List.app => <- <- /=. right. by left.
     + move=> [] <- <- ->. left. by exists s.
   - move=> x1 u IH [|y1 s].
     + rewrite ?app_nil_l. move=> <-. right. right. by exists (x1 :: u).
@@ -707,7 +707,7 @@ Proof.
         ** rewrite app_nil_r /= ?map_app. move: (a) => [|?]; first done.
            move=> Hi [] H1 [<-] H2.
            move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy.
-           inversion Hxy. subst.
+           inversion Hxy. subst. try rewrite [in LHS]/List.app in H1.
            eexists (u' ++ [sz]), v', (_ :: _).
            rewrite -?app_assoc. constructor; [done | by rewrite /= ?map_app H1 H2].
         ** rewrite ?map_app filter_app /= app_nil_r /step.