List.upto needs to be pushed down, ie called again

on result of first simplification:

eg if len l1 = i
  (l1 ++ l2)[:i] --> l1[:i] --> l1

Actually makes insertion_sort work less well, because
it allows          ((_ ++ [|_|]) ++ _)[:_]
to be turned into  (_ ++ _ :: _)[:_]
and putting the discard boundary at a cons is not yet supported

LiveVerif/src/LiveVerifExamples/insertion_sort.v

@@ -1,3 +1,4 @@
+(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *)
 Require Import coqutil.Sorting.Permutation.
 Require Import LiveVerif.LiveVerifLib.
 Require Import List Lia.
@@ -49,7 +50,18 @@ Derive insert SuchThat (fun_correct! insert) As insert_ok.
 .**/ { /**.
   assert (len (sort l1 ++ [|x|]) = \[i]+1) by (rewrite List.len_app; simpl; ZnWords).
   .**/ real_insert(p, i); /**.
-.**/ } /**.
+  2: {
+    replace (sort l1 ++ x :: l2) with ((sort l1 ++ [|x|]) ++ l2) by steps.
+    rewrite List.upto_app_discard_r by steps.
+    rewrite List.upto_pastend by steps.
+    reflexivity.
+  }
+.**/ } /*?.
+step. step. step. step. step. step. step. step. step. step. step. step.
+step.
+change (x :: l2) with ([|x|] ++ l2).
+rewrite List.from_app_discard_l.
+step. step. cbn. step.
 Qed.
 
 (* Insertion sort *)