diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e12d489..51baf38 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -24,12 +24,13 @@ jobs:
           opam-pin: false
 
       - name: Install opam dependencies
-        run:  |
-          opam pin add --no-action warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#a1ffc3f2e47d942ad9e1194dfb71f0783ead6d8a
+        run: |
+          # keep the Warblre ref in sync with the README
+          opam pin add --no-action warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#c7b021e61d580b6061f0b040ca04d8e1b40e9de4
           opam install . --deps-only
 
       - name: Dune build
-        run:  opam exec -- dune build
+        run: opam exec -- dune build
 
-      - name: Check compiled libraries (coqchk)
-        run: opam exec -- coqchk -silent --output-context $(cat _CoqProject) _build/default/*/*.vo
+      - name: Check compiled libraries (rocqchk)
+        run: opam exec -- rocqchk -silent --output-context -R _build/default Linden _build/default/*/*.vo
diff --git a/.gitignore b/.gitignore
index 97e54a7..b723a5e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,3 +10,4 @@ _build
 _opam
 \#*.*\#
 *.v~
+_RocqProject
diff --git a/Engine/BooleanSemantics.v b/Engine/BooleanSemantics.v
index 1184285..77e8fca 100644
--- a/Engine/BooleanSemantics.v
+++ b/Engine/BooleanSemantics.v
@@ -1,4 +1,4 @@
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -138,7 +138,7 @@ Inductive bool_encoding: LoopBool -> input -> actions -> Prop :=
     (ENCODE: bool_encoding b str cont),
     bool_encoding b str (Aclose gid::cont)
 | cons_true:
-  forall stk str head 
+  forall stk str head
     (ENCODE: bool_encoding CanExit str stk)
     (STRICT: strict_suffix str head forward),
     bool_encoding CanExit str (Acheck head::stk)
@@ -191,7 +191,7 @@ Proof.
   intros b str cont H.
   remember (Acheck str::cont) as prevcont.
   induction H; intros; auto; inversion Heqprevcont.
-  subst. apply ss_neq in STRICT. contradiction. 
+  subst. apply ss_neq in STRICT. contradiction.
 Qed.
 
 Lemma encode_next:
@@ -321,7 +321,7 @@ Proof.
   intros r str t PIKE H.
   eapply encode_equal; eauto.
   { constructor; constructor; auto. }
-  constructor. constructor. 
+  constructor. constructor.
 Qed.
 
 
diff --git a/Engine/Complexity.v b/Engine/Complexity.v
index f58db16..76c0132 100644
--- a/Engine/Complexity.v
+++ b/Engine/Complexity.v
@@ -1,6 +1,6 @@
 (** * Complexity of the PikeVM algorithm *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -232,7 +232,7 @@ Proof.
     assert (S (length next) > S n) by lia.
     specialize (IHn (c::pref) next H0). rewrite advance_S_n.
     simpl in IHn. simpl. lia.
-Qed.         
+Qed.
 
 
 (** * Well-formedness of the code  *)
@@ -245,7 +245,7 @@ Lemma compilation_nonempty:
   forall r, nonempty (compilation r).
 Proof.
   intros. unfold compilation. destruct compile. unfold nonempty, size.
-  rewrite app_length. simpl. lia.
+  rewrite length_app. simpl. lia.
 Qed.
 
 (* Some bytecode is well-formed if every target label belongs in some range *)
@@ -361,7 +361,7 @@ Proof.
   intros pc i next GET IN.
   assert (HL: pc < length (c ++ [Accept])).
   { eapply nth_error_Some. unfold get_pc in GET. rewrite GET. intros HI. inversion HI. }
-  rewrite app_length in HL. simpl in HL.
+  rewrite length_app in HL. simpl in HL.
   assert (pc = length c \/ pc < length c) as [ACC|H1] by lia.
   (* accept *)
   { subst. assert (get_pc (c ++ [Accept]) (length c) = get_pc [Accept] 0).
@@ -373,7 +373,7 @@ Proof.
   { unfold get_pc in GET. rewrite nth_error_app1 in GET; auto. }
   assert (POS: pc >= 0) by lia.
   specialize (nfa_wf r c 0 (length c) pc next i REP POS H1 GETI IN) as WF.
-  unfold size. rewrite app_length. simpl. lia.
+  unfold size. rewrite length_app. simpl. lia.
 Qed.
 
 Lemma eps_step_blocked_wf:
@@ -477,7 +477,7 @@ Proof.
       subst. unfold pike_vm_initial_thread. simpl. auto.
     + constructor.
     + intros n0 lit0 H. eapply search_in_range; eauto.
-    + unfold measure. simpl. rewrite free_initial. specialize (advance_n_inpsize inp n RANGEPREF)as ADV. 
+    + unfold measure. simpl. rewrite free_initial. specialize (advance_n_inpsize inp n RANGEPREF)as ADV.
       apply increase_mult with (x:= 4 * size code) in ADV as NEXT. simpl in NEXT. lia.
   (* end *)
   - exists 0. split.
@@ -498,7 +498,7 @@ Proof.
     + intros n lit0 H. eapply search_in_range; eauto.
     + unfold measure. simpl. rewrite free_initial. apply advance_input_decreases in ADVANCE.
       apply increase_mult with (x:= 4 * size code) in ADVANCE as NEXT. simpl in NEXT.
-      rewrite app_length. simpl. lia.
+      rewrite length_app. simpl. lia.
   (* nextchar_filter: we might add (2*codesize) free slots, but we lose an input length *)
   - exists (measure (size code) [] (thr::blocked) [] inp2). split; [constructor|]; auto.
     + constructor.
@@ -520,7 +520,7 @@ Proof.
     + unfold add_thread. apply wf_new; auto.
     + specialize (free_add seen (size code) dist (pc,gm,b) SEENWF UNSEEN) as FREE.
       apply wf_size in FREE; auto. apply eps_step_active in STEP0.
-      unfold measure, free. rewrite app_length. simpl. simpl in FREE. lia.
+      unfold measure, free. rewrite length_app. simpl. simpl in FREE. lia.
   (* match: we lose a thread and a free slot *)
   - assert (RANGE: pc < size code).
     { specialize (ACTIVEWF (pc,gm,b) ltac:(simpl;left;auto)). simpl in ACTIVEWF. auto. }
@@ -541,7 +541,7 @@ Proof.
          eapply eps_step_blocked_wf in STEP0 as [i [GET IN]]; eauto.
      + unfold add_thread. apply wf_new; auto.
      + specialize (free_add seen (size code) dist (pc,gm,b) SEENWF UNSEEN RANGE) as FREE.
-       apply wf_size in FREE. unfold measure, free. rewrite app_length. simpl. simpl in FREE. lia.
+       apply wf_size in FREE. unfold measure, free. rewrite length_app. simpl. simpl in FREE. lia.
 Qed.
 
 (** * Code Size  *)
@@ -579,23 +579,23 @@ Proof.
   - destruct (compile r1 (S start)) eqn:C1. destruct (compile r2 (S l)) eqn:C2.
     erewrite <- IHr1; eauto. 2: pike_subset.
     erewrite <- IHr2; eauto. 2: pike_subset.
-    inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+    inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
   - destruct (compile r1 start) eqn:C1. destruct (compile r2 l) eqn:C2.
     erewrite <- IHr1; eauto. 2: pike_subset.
     erewrite <- IHr2; eauto. 2: pike_subset.
-    inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+    inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
   - destruct min; destruct (destruct_delta delta) as [DZ | [D1 | [DINF | [delta' [DUN N3]]]]]; subst; try solve[pike_subset].
     + inversion COMP. auto.
     + destruct (compile r (S (S (S start)))) eqn:C1.
       erewrite <- IHr; eauto. 2: pike_subset.
-      inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+      inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
     + destruct (compile r (S (S (S start)))) eqn:C1.
       erewrite <- IHr; eauto. 2: pike_subset.
-      inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+      inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
     + inversion SUBSET; subst; lia.
   - destruct (compile r (S start)) eqn:C1.
     erewrite <- IHr; eauto. 2: pike_subset.
-    inversion COMP. subst. simpl. rewrite app_length. simpl. lia.
+    inversion COMP. subst. simpl. rewrite length_app. simpl. lia.
 Qed.
 
 Theorem compilation_size:
@@ -604,7 +604,7 @@ Theorem compilation_size:
     size (compilation r) = codesize r.
 Proof.
   unfold codesize, size, compilation. intros r H. destruct (compile r 0) eqn:COMP.
-  apply compile_size in COMP; auto. rewrite <- COMP. rewrite app_length. simpl. lia.
+  apply compile_size in COMP; auto. rewrite <- COMP. rewrite length_app. simpl. lia.
 Qed.
 
 (* relating this compilation size to the size of the regex *)
@@ -642,7 +642,7 @@ Proof.
   - unfold pike_vm_initial_state. rewrite <- compilation_size; auto.
     constructor; auto.
     + intros t H. destruct H. 2: inversion H.
-      subst. simpl. unfold compilation. destruct (compile r 0) eqn:C. unfold size. rewrite app_length.
+      subst. simpl. unfold compilation. destruct (compile r 0) eqn:C. unfold size. rewrite length_app.
       simpl. lia.
     + intros t H. inversion H.
     + constructor.
diff --git a/Engine/Correctness.v b/Engine/Correctness.v
index 388cd6e..03d05f8 100644
--- a/Engine/Correctness.v
+++ b/Engine/Correctness.v
@@ -1,6 +1,6 @@
 (** * Correctness theorems for the PikeVM engine  *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -254,7 +254,7 @@ Qed.
 (* Any execution of MemoBT to a final state corresponds to an execution of MemoTree *)
 Theorem memobt_to_memotree:
   forall r inp tree result,
-    pike_regex r -> 
+    pike_regex r ->
     bool_tree rer [Areg r] inp CanExit tree ->
     trc_memo_bt (compilation r) (MemoBT.initial_state inp) (MBT_final result) ->
     trc_memo_tree (initial_tree_state tree inp) (MTree_final result).
@@ -279,7 +279,7 @@ Proof.
   apply IHTRC. eapply memotree_preservation; eauto.
 Qed.
 
-  
+
 (** * Correctness Theorem of the PikeVM result  *)
 
 Theorem memobt_correct:
diff --git a/Engine/FunctionalPikeVM.v b/Engine/FunctionalPikeVM.v
index 1ba0b56..d917147 100644
--- a/Engine/FunctionalPikeVM.v
+++ b/Engine/FunctionalPikeVM.v
@@ -1,6 +1,6 @@
 (* The PikeVm algorithm, expressed as a fuel-based function *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -76,7 +76,7 @@ Fixpoint pike_vm_loop (c:code) (pvs:pike_vm_state) (fuel:nat) : pike_vm_state :=
 
 (* an upper bound for the fuel necessary to compute a result *)
 Definition vm_fuel (r:regex) (inp:input) : nat :=
-  complexity r inp. 
+  complexity r inp.
 
 Inductive matchres : Type :=
 | OutOfFuel
@@ -206,7 +206,7 @@ End FunctionalPikeVM.
 
 From Linden Require Import Inst.
 From Warblre Require Import Inst.
-Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Stdlib.Strings.Ascii Stdlib.Strings.String.
 Open Scope string_scope.
 
 Section Example.
diff --git a/Engine/MemoBT.v b/Engine/MemoBT.v
index 230496b..fde62b8 100644
--- a/Engine/MemoBT.v
+++ b/Engine/MemoBT.v
@@ -1,7 +1,7 @@
 (** * MemoBT algorithm  *)
 (* A backtracking algorithm on the extended NFA, with memoization *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -35,7 +35,7 @@ Section MemoBT.
     MBT [(0, GroupMap.empty, CanExit, inp)] initial_memoset.
 
   (** * MemoBT small-step semantics *)
-  
+
   Inductive exec_result : Type :=
   | FoundMatch: leaf -> exec_result
   | Explore: stack -> exec_result.
@@ -77,7 +77,7 @@ Section MemoBT.
         end
     end.
 
-  
+
   Inductive memobt_step (c:code) : mbt_state -> mbt_state -> Prop :=
   (* we exhausted all configurations, there is no match *)
   | mbt_nomatch: forall ms,
@@ -102,7 +102,7 @@ Section MemoBT.
 
   (** * MemoBT properties  *)
 
-  Theorem memobt_deterministic: 
+  Theorem memobt_deterministic:
      forall c mbs mbs1 mbs2
     (STEP1: memobt_step c mbs mbs1)
     (STEP2: memobt_step c mbs mbs2),
diff --git a/Engine/MemoEquiv.v b/Engine/MemoEquiv.v
index 42778ac..eb71628 100644
--- a/Engine/MemoEquiv.v
+++ b/Engine/MemoEquiv.v
@@ -1,6 +1,6 @@
 (** * Equivalence between MemoBT algorithm and MemoTree algorithm  *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 
@@ -16,7 +16,7 @@ Section MemoEquiv.
   Context {params: LindenParameters}.
   Context {MS: MemoSet params}.
   Context (rer: RegExpRecord).
-  
+
   (* FIXME: these are generalizations of definitions used in the PikeEquiv proof *)
   (* it could be nice to only use the generalized version everywhere *)
   (* I should write an NFA library *)
@@ -77,7 +77,7 @@ Section MemoEquiv.
       simpl in IHTC1. destruct IHTC1; subst; simpl; auto.
   Qed.
 
-  
+
   Lemma tc_same_tree:
     forall code inp t1 gm1 t2 gm2 pc b
       (TC1: tree_config code (t1,gm1,inp) (pc,gm1,b,inp))
@@ -88,7 +88,7 @@ Section MemoEquiv.
     eapply tc_same_interm in TC1; eauto. simpl in TC1. auto.
   Qed.
 
-  
+
   (* the initial active config and the initial active tree are related with the invariant *)
   Lemma initial_tree_config:
     forall r code tree inp
@@ -117,7 +117,7 @@ Section MemoEquiv.
       (LTC: list_tree_config code treelist threadlist)
       (TC: tree_config code (tree, gm, inp) (pc, gm, b, inp)),
       list_tree_config code ((tree,gm,inp)::treelist) ((pc,gm,b,inp)::threadlist).
-  
+
   Lemma ltc_app:
     forall code tl1 tl2 vl1 vl2
       (LTC1: list_tree_config code tl1 vl1)
@@ -153,14 +153,14 @@ Section MemoEquiv.
     unfold seen_inclusion in *.
     intros pc0 b0 inp0 SEEN. apply is_memo_add in SEEN. destruct SEEN as [EQ|SEEN].
     - inversion EQ. subst. left. exists tree. exists gm. split; auto. apply in_add. left. auto.
-    - specialize (INCL pc0 b0 inp0 SEEN).      
+    - specialize (INCL pc0 b0 inp0 SEEN).
       destruct INCL as [[ts [gms [SEENs TTs]]] | [ST [ts [gms [GEQ [EQ TTS]]]]]].
       + left. exists ts. exists gms. split; auto. apply in_add. right; auto.
       + left. exists ts. exists gms. split; auto.
         apply in_add. left; auto. inversion EQ. auto.
   Qed.
 
-  
+
   Lemma skip_inclusion:
     forall code inp treeseen memoset tree gm currentpc
       (INCL: seen_inclusion code treeseen memoset (Some (tree, gm, inp)) currentpc)
@@ -197,7 +197,7 @@ Section MemoEquiv.
     - right. split; auto. exists ts. exists gms. split; auto. lia.
   Qed.
 
-  
+
   Definition head_pc (stk:list config) : label :=
     match stk with
     | [] => 0
@@ -332,7 +332,7 @@ Section MemoEquiv.
       repeat invert_rep. simpl. rewrite CONSUME, READ. split; auto. split; auto.
       eapply tc_eq; eauto.
       2: { pike_subset. }
-      replace (pc + 1) with (S pc) by lia. auto.      
+      replace (pc + 1) with (S pc) by lia. auto.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
       repeat (econstructor; eauto). pike_subset.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
@@ -358,7 +358,7 @@ Section MemoEquiv.
     - repeat invert_rep. simpl. rewrite OPEN. split; auto.
       eapply tc_eq; eauto.
       2: { pike_subset. }
-      replace (pc+1) with (S pc) by lia. 
+      replace (pc+1) with (S pc) by lia.
       apply cons_bc with (pcmid:=end1); repeat (econstructor; eauto).
   Qed.
 
@@ -375,7 +375,7 @@ Section MemoEquiv.
     induction TREE; intros; subst; try inversion HeqTCLOSE; subst.
     - repeat invert_rep. simpl. rewrite CLOSE. split; auto.
       econstructor; eauto. 2: pike_subset.
-      replace (pc + 1) with (S pc) by lia. auto. 
+      replace (pc + 1) with (S pc) by lia. auto.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
     - repeat invert_rep. eapply IHTREE; eauto. pike_subset.
       repeat (econstructor; eauto). pike_subset.
@@ -383,7 +383,7 @@ Section MemoEquiv.
     - destruct greedy; inversion CHOICE.
   Qed.
 
-  Lemma exec_reset:  
+  Lemma exec_reset:
     forall gidl tree inp code pc b gm,
       tree_config code (GroupAction (Reset gidl) tree, gm, inp) (pc,gm,b,inp)  ->
       stutters pc code = false ->
@@ -436,7 +436,7 @@ Section MemoEquiv.
     - repeat invert_rep. simpl. rewrite CHECK, ANCHOR. split; auto.
       eapply tc_eq; eauto.
       2: { pike_subset. }
-      replace (pc+1) with (S pc) by lia. 
+      replace (pc+1) with (S pc) by lia.
       assumption.
   Qed.
 
@@ -502,7 +502,7 @@ Section MemoEquiv.
               { constructor. replace (S pc+1+1) with (S (S (S pc))) by lia. auto. }
               repeat (econstructor; eauto).
             * apply tc_eq with (actions:=cont); auto. pike_subset.
-        }      
+        }
       + { (* Star *)
           destruct plus; inversion DINF.
           repeat invert_rep. destruct greedy; inversion CHOICE; subst.
@@ -670,14 +670,14 @@ Section MemoEquiv.
         exists pcstart. exists b. split; try split; try lia.
         * simpl. rewrite JMP. auto.
         * apply tc_eq with (actions:=Areg (Quantified greedy 0 (NoI.N 1 + NoI.N 0)%NoI r1) :: cont); try constructor; auto; pike_subset.
-          eapply tree_quant_free; eauto.        
+          eapply tree_quant_free; eauto.
       (* Star *)
       + destruct plus; inversion DINF. invert_rep.
         { invert_rep. invert_rep; try in_subset. destruct greedy; stutter. }
         exists pcstart. exists b. split; try split; try lia.
         * simpl. rewrite JMP. auto.
         * apply tc_eq with (actions:=Areg (Quantified greedy 0 (NoI.N 1 + +∞)%NoI r1) :: cont); try constructor; auto; pike_subset.
-          eapply tree_quant_free; eauto.        
+          eapply tree_quant_free; eauto.
       (* Unsupported *)
       + rewrite DUN in SUBSET. inversion SUBSET; inversion H1; inversion H4; subst; lia.
     - invert_rep.
@@ -722,7 +722,7 @@ Section MemoEquiv.
       unfold PikeVM.upd_label. eauto.
   Qed.
 
-  
+
 
   Theorem invariant_preservation:
   forall code mts1 mbs1 mbs2
diff --git a/Engine/MemoTree.v b/Engine/MemoTree.v
index 50bbb42..3744fde 100644
--- a/Engine/MemoTree.v
+++ b/Engine/MemoTree.v
@@ -1,7 +1,7 @@
 (** * MemoTree algorithm  *)
 (* A backtracking algorithm, with memoization, on trees *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -19,7 +19,7 @@ Section MemoTree.
   (* configurations to be explored by the memoized backtracking engine *)
   Definition tree_config: Type := tree * group_map * input.
   Definition tree_stack: Type := list tree_config.
-  
+
   (* states of the MemoBT algorithm *)
   Inductive mtree_state : Type :=
   | MTree (stk:tree_stack) (ts: seentrees): mtree_state
@@ -70,7 +70,7 @@ Section MemoTree.
     forall ts t gm i nextconfs stk
       (EXPLORE: exec_tree (t,gm,i) = TExplore nextconfs),
       memotree_step (MTree ((t,gm,i)::stk) ts) (MTree (nextconfs++stk) (add_seentrees ts t)).
-  
+
   (** * MemoTree properties  *)
 
   Theorem memotree_progress:
@@ -102,17 +102,17 @@ Section MemoTree.
 
   (* This uses the non-deterministic results of the stack, just like the PikeTree proof. *)
   (* Such results can non-deteterministically skip any subtree in the seen set *)
-  
+
   (** * Initialization  *)
   (* In the initial state, the invariant holds *)
 
   Lemma init_memotree_inv:
     forall t inp,
-      pike_subtree t -> 
+      pike_subtree t ->
       memotree_inv (initial_tree_state t inp) (first_leaf t inp).
   Proof.
     intros t. unfold first_leaf. unfold initial_tree_state. constructor; simpl; pike_subset; auto.
-    intros res LISTND. 
+    intros res LISTND.
     simpl. apply tree_nd_initial; auto.
     inversion LISTND; subst. inversion TLR; subst. rewrite seqop_none. auto.
   Qed.
@@ -225,5 +225,5 @@ Section MemoTree.
       + econstructor; eauto.
         eapply list_add_seen_nd with (gm:=gm) in TLR; eauto.
   Qed.
-  
+
 End MemoTree.
diff --git a/Engine/Meta.v b/Engine/Meta.v
index 8429462..3e80c78 100644
--- a/Engine/Meta.v
+++ b/Engine/Meta.v
@@ -8,7 +8,7 @@
 (* encapsulating heuristics that look for matches using strategies it deems *)
 (* to be the most efficient. *)
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Semantics Tree.
diff --git a/Engine/NFA.v b/Engine/NFA.v
index 277e224..85cbc49 100644
--- a/Engine/NFA.v
+++ b/Engine/NFA.v
@@ -1,4 +1,4 @@
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -234,26 +234,26 @@ Section NFA.
     - inversion COMPILE.
       destruct (compile r1 (S fresh)) as [bc1 f1] eqn:COMP1. destruct (compile r2 (S f1)) as [bc2 f2] eqn:COMP2.
       inversion H0. subst f2. apply IHr1 in COMP1. apply IHr2 in COMP2. simpl.
-      rewrite <- COMP1 in COMP2. simpl in COMP2. rewrite app_length. simpl. lia.
+      rewrite <- COMP1 in COMP2. simpl in COMP2. rewrite length_app. simpl. lia.
     - inversion COMPILE.
       destruct (compile r1 fresh) as [bc1 f1] eqn:COMP1. destruct (compile r2 f1) as [bc2 f2] eqn:COMP2.
       inversion H0. subst f2. apply IHr1 in COMP1. apply IHr2 in COMP2.
-      rewrite <- COMP1 in COMP2. rewrite app_length. lia.
+      rewrite <- COMP1 in COMP2. rewrite length_app. lia.
     - inversion COMPILE. destruct min.
       2: { inversion H0. simpl. lia. }
       destruct delta.
       + destruct n; try destruct n; try solve[inversion H0; simpl; lia].
-        destruct (compile r (S (S (S fresh)))) as [bc1 f1] eqn:COMP1. 
+        destruct (compile r (S (S (S fresh)))) as [bc1 f1] eqn:COMP1.
         inversion H0. apply IHr in COMP1.
-        subst. simpl. rewrite app_length. simpl. lia.
-      + destruct (compile r (S (S (S fresh)))) as [bc1 f1] eqn:COMP1. 
+        subst. simpl. rewrite length_app. simpl. lia.
+      + destruct (compile r (S (S (S fresh)))) as [bc1 f1] eqn:COMP1.
         inversion H0. apply IHr in COMP1.
-        subst. simpl. rewrite app_length. simpl. lia.
+        subst. simpl. rewrite length_app. simpl. lia.
     - inversion COMPILE.
       destruct (compile r (S fresh)) as [bc1 f1] eqn:COMP1. inversion H0. apply IHr in COMP1.
-      subst. simpl. rewrite app_length. simpl. lia.
-  Qed.    
-  
+      subst. simpl. rewrite length_app. simpl. lia.
+  Qed.
+
   (* this shows that the compilation function adheres to the representation predicate *)
   Theorem compile_nfa_rep:
     forall r c start endl prev,
@@ -268,7 +268,7 @@ Section NFA.
       inversion H2. subst. apply nfa_rep_disj with (end1:=end1).
       + rewrite get_first. simpl. auto.
       + apply IHr1 with (prev:=prev ++ [Fork (S (length prev)) (S end1)]) in COMP1.
-        2: { rewrite app_length. simpl. lia. }
+        2: { rewrite length_app. simpl. lia. }
         replace (prev ++ Fork (S (length prev)) (S end1) :: bc1 ++ Jmp endl :: bc2) with
           (((prev ++ [Fork (S (length prev)) (S end1)]) ++ bc1) ++ (Jmp endl :: bc2)).
         2:{ rewrite <- app_assoc. rewrite <- app_assoc. auto. }
@@ -282,14 +282,14 @@ Section NFA.
           2: { rewrite <- app_assoc. simpl. apply f_equal. apply f_equal. rewrite <- app_assoc. auto. }
           auto.
         * apply fresh_correct in COMP1. rewrite <- COMP1. simpl.
-          rewrite app_length. simpl. rewrite app_length. simpl. lia.
+          rewrite length_app. simpl. rewrite length_app. simpl. lia.
     - inversion H. destruct (compile r1 start) as [bc1 end1] eqn:COMP1. destruct (compile r2 end1) as [bc2 end2] eqn:COMP2.
       inversion H2. subst. econstructor.
       + apply IHr1 with (prev:=prev) in COMP1; auto.
         rewrite app_assoc. apply nfa_rep_extend. eauto.
       + apply IHr2 with (prev:=prev ++ bc1) in COMP2; auto.
         * rewrite app_assoc. auto.
-        * apply fresh_correct in COMP1. rewrite app_length. lia.
+        * apply fresh_correct in COMP1. rewrite length_app. lia.
     - inversion H. destruct min.
       2: { inversion H2. subst. apply nfa_unsupported.
           - unfold not. intros. inversion H0.
@@ -308,12 +308,12 @@ Section NFA.
                ((prev ++ greedy_fork greedy (S (length prev)) (S end1) :: BeginLoop :: ResetRegs (def_groups r) :: bc1) ++ [EndLoop (S end1)]).
              2: { rewrite <- app_assoc. auto. }
              apply nfa_rep_extend. auto.
-          ** rewrite app_length. simpl. lia.
+          ** rewrite length_app. simpl. lia.
         * replace (prev ++ greedy_fork greedy (S (length prev)) (S end1) :: BeginLoop :: ResetRegs (def_groups r) :: bc1 ++ [EndLoop (S end1)]) with
             ((prev ++ greedy_fork greedy (S (length prev)) (S end1) :: BeginLoop :: ResetRegs (def_groups r) :: bc1) ++ [EndLoop (S end1)]).
           2: { rewrite <- app_assoc. auto. }
           apply fresh_correct in COMP1. subst. apply get_first_0.
-          simpl. rewrite app_length. simpl. lia.
+          simpl. rewrite length_app. simpl. lia.
       (* Star *)
       + destruct (compile r (S (S (S start)))) as [bc1 end1] eqn:COMP1. inversion H2. subst. constructor.
         * rewrite get_first. simpl. auto.
@@ -325,12 +325,12 @@ Section NFA.
                ((prev ++ greedy_fork greedy (S (length prev)) (S end1) :: BeginLoop :: ResetRegs (def_groups r) :: bc1) ++ [EndLoop (length prev)]).
              2: { rewrite <- app_assoc. auto. }
              apply nfa_rep_extend. auto.
-          ** rewrite app_length. simpl. lia.
+          ** rewrite length_app. simpl. lia.
         * replace (prev ++ greedy_fork greedy (S (length prev)) (S end1) :: BeginLoop :: ResetRegs (def_groups r) :: bc1 ++ [EndLoop (length prev)]) with
             ((prev ++ greedy_fork greedy (S (length prev)) (S end1) :: BeginLoop :: ResetRegs (def_groups r) :: bc1) ++ [EndLoop (length prev)]).
           2: { rewrite <- app_assoc. auto. }
           apply fresh_correct in COMP1. subst. apply get_first_0.
-          simpl. rewrite app_length. simpl. lia.
+          simpl. rewrite length_app. simpl. lia.
       (* Unsupported *)
       + assert (([KillThread], S start) = (c,endl)).
         { destruct delta'; auto. lia. destruct delta'; auto. lia. }
@@ -344,13 +344,13 @@ Section NFA.
       constructor.
       + rewrite get_first. simpl. auto.
       +  apply IHr with (prev:=prev ++ [SetRegOpen id]) in COMP1.
-        2: { rewrite app_length. simpl. lia. }
+        2: { rewrite length_app. simpl. lia. }
         replace (prev ++ SetRegOpen id :: bc1 ++ [SetRegClose id]) with ((prev ++ SetRegOpen id :: bc1) ++ [SetRegClose id]).
         2:{ rewrite <- app_assoc. auto. }
         apply nfa_rep_extend. rewrite <- app_assoc in COMP1. simpl in COMP1. auto.
       + replace (prev ++ SetRegOpen id :: bc1 ++ [SetRegClose id]) with ((prev ++ SetRegOpen id :: bc1) ++ [SetRegClose id]).
         2:{ rewrite <- app_assoc. auto. }
-        apply get_first_0. apply fresh_correct in COMP1. subst. rewrite app_length. simpl. lia.
+        apply get_first_0. apply fresh_correct in COMP1. subst. rewrite length_app. simpl. lia.
     - inversion H. subst. constructor. apply get_first.
     - inversion H. subst. apply nfa_unsupported.
       + unfold not. intros. inversion H0.
diff --git a/Engine/PikeEquiv.v b/Engine/PikeEquiv.v
index c7b067a..eb44c87 100644
--- a/Engine/PikeEquiv.v
+++ b/Engine/PikeEquiv.v
@@ -1,6 +1,6 @@
 (* Relating the PikeVM smallstep semantics to the Pike Tree smallstep semantics *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -859,7 +859,7 @@ Qed.
 Lemma next_prefix_counter_none_nores {strs:StrSearch}:
   forall r inp future,
     pike_regex r ->
-    future_tree_shape rer r inp future -> 
+    future_tree_shape rer r inp future ->
     next_prefix_counter inp (extract_literal rer r) = None ->
     first_leaf future inp = None.
 Proof.
@@ -876,7 +876,7 @@ Proof.
     pose proof (not_found _ _ Hsearch 0 ltac:(lia)) as Hnostart.
     let inp := constr:(Input next (c::pref)) in
     replace (skipn 0 next) with (next_str inp) in Hnostart by easy.
-    eapply extract_literal_prefix_contra in Hnostart; eauto. 
+    eapply extract_literal_prefix_contra in Hnostart; eauto.
     unfold first_leaf in Hnostart |- *. simpl. unfold advance_input'. simpl.
     rewrite Hnostart. simpl.
     (* IH for titer *)
@@ -1050,7 +1050,7 @@ Proof.
   2: { inversion H. }
   assert (HL: pc < length (r_code ++ [Accept])).
   { eapply nth_error_Some. rewrite NTH. intros HI. inversion HI. }
-  rewrite app_length in HL. simpl in HL.
+  rewrite length_app in HL. simpl in HL.
   assert (pc = length (r_code) \/ pc < length (r_code)) as [ACC|H1] by lia.
   (* accept *)
   { subst. assert (get_pc (r_code ++ [Accept]) (length r_code) = get_pc [Accept] 0).
@@ -1207,7 +1207,7 @@ Proof.
             -- eapply pikeinv; eauto using initial_tree_thread, initial_inclusion, ltt_app, ltt_cons, ltt_nil, future_nextprefix_some.
           * eexists. split.
             -- eapply pts_nextchar_generate; eauto using erases, next_prefix_counter_none_nores.
-            -- eauto using pikeinv, initial_tree_thread, initial_inclusion, ltt_app, ltt_cons, ltt_nil, nnp_none. 
+            -- eauto using pikeinv, initial_tree_thread, initial_inclusion, ltt_app, ltt_cons, ltt_nil, nnp_none.
       (* nextchar_filter *)
       + assert (pvs2 = PVS (Input next (c::pref)) ((pc,gmblocked,b)::threadlist) best [] (Some (nextprefix, lit)) initial_seenpcs)
            by eauto using pikevm_deterministic, pvs_nextchar_filter.
diff --git a/Engine/PikeSubset.v b/Engine/PikeSubset.v
index dc10cc8..5cfad85 100644
--- a/Engine/PikeSubset.v
+++ b/Engine/PikeSubset.v
@@ -1,4 +1,4 @@
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -105,7 +105,7 @@ Section PikeSubset.
     forall t gm i l,
       pike_list ((t,gm,i)::l) <-> pike_subtree t /\ pike_list l.
   Proof.
-    intros t gm i l. unfold pike_list. split; try split; intros. 
+    intros t gm i l. unfold pike_list. split; try split; intros.
     - eapply H; eauto. left. eauto.
     - eapply H; eauto. right. eauto.
     - destruct H. inversion H0; subst.
@@ -159,19 +159,19 @@ Section PikeSubset.
   Proof.
     intros l1 l2 inp. unfold suppl. rewrite map_app. auto.
   Qed.
-  
+
 End PikeSubset.
 
 
 
 (* inverting evidence of belonging to the subset *)
-Ltac invert_subset := 
+Ltac invert_subset :=
   match goal with
   | [ H : pike_list (suppl ((_, _) :: _) _) |- _ ] => simpl in H
   | [ H : pike_list ((_,_,_)::_) |- _ ] => apply pike_list_cons in H; destruct H
   | [ H : pike_list (?tgmi::_) |- _ ] => destruct ?tgmi as [[t gm]i]
   | [ H : pike_list (_ ++ _) |- _ ] => apply pike_list_app in H; destruct H
-    
+
   | [ H : pike_subtree (Choice _ _) |- _ ] => inversion H; clear H
   | [ H : pike_subtree (Read _ _) |- _ ] => inversion H; clear H
   | [ H : pike_subtree (Progress _) |- _ ] => inversion H; clear H
@@ -179,12 +179,12 @@ Ltac invert_subset :=
   | [ H : pike_subtree (ReadBackRef _ _) |- _ ] => inversion H; clear H
   | [ H : pike_subtree (AnchorPass _ _) |- _ ] => inversion H; clear H
   | [ H : pike_subtree (LK _ _ _) |- _ ] => inversion H; clear H
-  | [ H : pike_subtree (LKFail _ _) |- _ ] => inversion H; clear H                                       
+  | [ H : pike_subtree (LKFail _ _) |- _ ] => inversion H; clear H
 
   | [ H : pike_actions (_ :: _) |- _ ] => inversion H; clear H
 
   | [ H : pike_action (Areg _) |- _ ] => inversion H; clear H
-                                                           
+
   | [ H : pike_regex (Regex.Character _) |- _ ] => inversion H; clear H
   | [ H : pike_regex (Disjunction _ _) |- _ ] => inversion H; clear H
   | [ H : pike_regex (Sequence _ _) |- _ ] => inversion H; clear H
@@ -231,11 +231,11 @@ Section PikeSubsetLemma.
   Proof.
     intros rer cont inp gm dir t PIKE ISTREE.
     induction ISTREE; try apply IHISTREE; pike_subset; auto.
-    - apply IHISTREE1. pike_subset. 
+    - apply IHISTREE1. pike_subset.
     - apply IHISTREE2. pike_subset.
-    - destruct dir; simpl; pike_subset. 
+    - destruct dir; simpl; pike_subset.
     - destruct greedy.
-      + pike_subset. apply IHISTREE1. destruct plus; inversion H3. pike_subset. 
+      + pike_subset. apply IHISTREE1. destruct plus; inversion H3. pike_subset.
       + pike_subset. apply IHISTREE1. destruct plus; inversion H3. pike_subset.
     - destruct greedy.
       + pike_subset. apply IHISTREE1. destruct plus; inversion H3. pike_subset.
diff --git a/Engine/PikeTree.v b/Engine/PikeTree.v
index acee90b..52f2575 100644
--- a/Engine/PikeTree.v
+++ b/Engine/PikeTree.v
@@ -7,9 +7,9 @@
 (* all the trees it has already started to explore *)
 (* Non-deterministically, it can decide not to explore a tree it has already seen *)
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 From Linden Require Import Regex Chars Groups Tree.
 From Linden Require Import PikeSubset SeenSets.
@@ -259,7 +259,7 @@ Section PikeTree.
     - pike_subset. specialize (IHtree_nd1 H3 (@eq_refl _ _)).
       specialize (IHtree_nd2 H4 (@eq_refl _ _)). subst. auto.
   Qed.
-  
+
   (** * List Results  *)
   (* first possible result in a list of trees - deterministic and non-deterministic versions *)
 
@@ -301,7 +301,7 @@ Section PikeTree.
   (* the normal result for a list, without skipping anything, is a possible result *)
   Lemma list_result_nd:
     forall active seen,
-      pike_list active -> 
+      pike_list active ->
       list_nd active seen (list_result active).
   Proof.
     intros active. induction active; try destruct a as [[t gm] i]; intros; pike_subset; try constructor.
@@ -370,8 +370,8 @@ Section PikeTree.
     eapply state_nd_future_none; eauto using res_group_map_indep.
   Qed.
 
-    
-  
+
+
   (** * Initialization  *)
 
   (* In the initial state, the invariant holds *)
@@ -662,7 +662,7 @@ Section PikeTree.
       2:{ simpl; pike_subset. }
       2:{ destruct next_future; auto. inversion ERASE; subst; pike_subset. }
       econstructor; try econstructor. unfold next_inp, advance_input', advance_input.
-      simpl. subst. 
+      simpl. subst.
       rewrite suppl_app, list_result_app, <-seqop_assoc.
       unfold list_result at 2, seqop_list. simpl.
       inversion ERASE; subst; simpl.
diff --git a/Engine/PikeVM.v b/Engine/PikeVM.v
index b192c4a..1142b4d 100644
--- a/Engine/PikeVM.v
+++ b/Engine/PikeVM.v
@@ -3,7 +3,7 @@
 (* The PikeVM algorithm, expressed as small-step semantics on the bytecode NFA *)
 (* It records the code labels it has already handled to avoid doing work twice *)
 
-(* 
+(*
 Anchored vs unanchored PikeVM:
 
 The PikeVM can operate in two modes: anchored and unanchored. Which mode we operate
@@ -34,7 +34,7 @@ and blocked thread, we can do the "acceleration" step, where we jump ahead in th
 to the next position where the prefix matches.
 *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
diff --git a/Engine/Prefix.v b/Engine/Prefix.v
index 1d383d6..a0409d6 100644
--- a/Engine/Prefix.v
+++ b/Engine/Prefix.v
@@ -6,7 +6,7 @@
 (* do not contain this prefix. In some cases, this even allows us to skip *)
 (* the entire regex engine and just use a substring search. *)
 
-Require Import List Lia RelationClasses FunInd Recdef Arith.
+From Stdlib Require Import List Lia RelationClasses FunInd Recdef Arith.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Semantics Tree FunctionalSemantics.
@@ -109,7 +109,7 @@ Proof.
   destruct ss as [|c ss'].
   - destruct i; [lia|].
     apply (no_earlier _ _ _ H i ltac:(lia)). constructor.
-  - assert (Hlen: length (skipn i s) = 0) by (rewrite skipn_length; lia).
+  - assert (Hlen: length (skipn i s) = 0) by (rewrite length_skipn; lia).
     destruct (skipn i s); [inversion Hsw|discriminate].
 Qed.
 
@@ -270,7 +270,7 @@ Proof.
   apply ss_fwd_diff in Hss as [diff [Hdiff [Hnext Hpref]]].
   exists (length diff). repeat split.
   - rewrite <-length_zero_iff_nil in Hdiff. lia.
-  - subst. simpl. rewrite app_length. lia.
+  - subst. simpl. rewrite length_app. lia.
   - simpl. rewrite Hnext, skipn_app.
     replace (length diff - length diff) with 0 by lia.
     now rewrite skipn_all2 by lia.
@@ -304,7 +304,7 @@ Proof.
       apply ss_fwd_diff in Hss2 as [diff [Hdiff [Hnext _]]]. subst.
       rewrite <-length_zero_iff_nil in Hdiff.
       apply f_equal with (f:=@length Character) in Hnext.
-      rewrite app_length, !skipn_length in Hnext. lia.
+      rewrite length_app, !length_skipn in Hnext. lia.
     }
     now apply Hne.
 Qed.
@@ -407,7 +407,7 @@ Lemma chain_literals_length:
     length (prefix (chain_literals l1 l2)) <= length (prefix l1) + length (prefix l2).
 Proof.
   intros l1 l2.
-  destruct l1, l2; simpl; try rewrite app_length; lia.
+  destruct l1, l2; simpl; try rewrite length_app; lia.
 Qed.
 
 Lemma repeat_literal_length:
@@ -523,7 +523,7 @@ Fixpoint extract_literal_char (cd: char_descr) : literal :=
   end.
 
 (* extracting literals from a regex *)
-(* 
+(*
   TODO: this could benefit from a few improvements:
   - Support lookarounds by performing intersection of overlapping literals.
     For instance /(?=abc)p/ => None, /(?<=abc)c/ => 'c' (but not exact nor prefix). This would require thinking reconsidering what Exact and Prefix mean.
@@ -745,7 +745,7 @@ Proof.
   (* tree_sequence *)
   - simpl in Hextract, IHHtree.
     destruct_i.
-    + destruct extract_actions_literal; try easy. 
+    + destruct extract_actions_literal; try easy.
       repeat rewrite chain_literals_impossible in IHHtree.
       eapply IHHtree; eauto.
     + rewrite chain_literals_assoc in IHHtree.
diff --git a/Engine/SeenSets.v b/Engine/SeenSets.v
index 3892ccc..f3c0340 100644
--- a/Engine/SeenSets.v
+++ b/Engine/SeenSets.v
@@ -1,4 +1,4 @@
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups Tree.
@@ -30,11 +30,11 @@ Class TSeen (params:LindenParameters) :=
 #[refine]
 Instance TSlist (params:LindenParameters) : TSeen params :=
   { seentrees := list tree;
-    
+
     initial_seentrees := [];
-    
+
     add_seentrees (s:list tree) (t:tree) := t::s;
-    
+
     inseen (s:list tree) (t:tree) :=
       List.existsb (fun x => tree_eqb x t) s;
   }.
@@ -66,10 +66,10 @@ Class VMSeen :=
 (* one instantiation using lists, but you could use anything else *)
 Definition lblbool_eq_dec : forall (l1 l2 : (label*LoopBool)), { l1 = l2 } + { l1 <> l2 }.
 Proof. repeat decide equality. Defined.
-  
+
 Definition lblbool_eqb l1 l2 : bool :=
   match lblbool_eq_dec l1 l2 with | left _ => true | _ => false end.
-  
+
 #[refine]
   Instance VMSlist : VMSeen :=
   { seenpcs := list (label * LoopBool);
@@ -132,4 +132,3 @@ Definition mbt_state_eqb {params:LindenParameters} s1 s2 : bool :=
 (* initial_empty *)
 - auto.
 Defined.
-
diff --git a/Engine/TreeRep.v b/Engine/TreeRep.v
index 12a4a31..fd36ac6 100644
--- a/Engine/TreeRep.v
+++ b/Engine/TreeRep.v
@@ -1,4 +1,4 @@
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -94,7 +94,7 @@ Inductive tree_rep: tree -> code -> label -> input -> LoopBool -> Prop :=
 Ltac same_instr :=
   match goal with
   | [ H1 : get_pc ?code ?pc = ?i1, H2: get_pc ?code ?pc = ?i2 |- _ ] => rewrite H1 in H2; inversion H2; subst
-  end.                                                                                                       
+  end.
 
 (* Determinism of the tree representation *)
 Theorem tree_rep_determ:
diff --git a/README.md b/README.md
index c2bacc2..57fa2c2 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,4 @@
-Linden: A Linear Dependable Engine for JavaScript Regular Expressions
-=====================================================================
+# Linden: A Linear Dependable Engine for JavaScript Regular Expressions
 
 [Project Page](https://aurele-barriere.github.io/linden.html)
 
@@ -17,10 +16,11 @@ Authors: [Aurèle Barrière](https://aurele-barriere.github.io/), [Victor Deng](
 
 This repository contains mechanized proofs, in Rocq, about JavaScript Regular Expressions.
 This includes:
-- a new *backtracking tree* semantics for JavaScript regexes, in folder `Semantics`.
+
+- a new _backtracking tree_ semantics for JavaScript regexes, in folder `Semantics`.
 - a proof that this semantics is equivalent to the [Warblre](https://github.com/epfl-systemf/Warblre) mechanization of JavaScript regexes, in folder `WarblreEquiv`.
 - a proof of the PikeVM linear-time matching algorithm supporting a subset of JavaScript regexes, in folder `Engine`. The algorithm is adapted to fit JavaScript unique quantifier semantics, following section 4.1 of [Linear Matching of JavaScript Regular Expressions](https://dl.acm.org/doi/10.1145/3656431).
-- proof of JavaScript regex *contextual equivalences*, in folder `Rewriting`.
+- proof of JavaScript regex _contextual equivalences_, in folder `Rewriting`.
 
 # Usage
 
@@ -33,7 +33,7 @@ This includes:
 2. Pin the version of Warblre:
 
    ```
-   opam pin add --no-action warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#a1ffc3f2e47d942ad9e1194dfb71f0783ead6d8a
+   opam pin add --no-action warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#c7b021e61d580b6061f0b040ca04d8e1b40e9de4
    ```
 
 3. Install dependencies:
diff --git a/Rewriting/Equivalence.v b/Rewriting/Equivalence.v
index 9a272fd..9266483 100644
--- a/Rewriting/Equivalence.v
+++ b/Rewriting/Equivalence.v
@@ -1,4 +1,4 @@
-From Coq Require Export Bool Arith List Equivalence Lia.
+From Stdlib Require Export Bool Arith List Equivalence Lia.
 From Warblre Require Import Base RegExpRecord.
 From Linden Require Import Regex Chars Groups Tree Semantics
   FunctionalSemantics FunctionalUtils ComputeIsTree Parameters
@@ -44,14 +44,14 @@ Section Definitions.
         (TREE1: is_tree rer acts1 inp gm dir t1)
         (TREE2: is_tree rer acts2 inp gm dir t2),
         tree_equiv_tr_dir inp gm dir t1 t2.
-    
+
     Definition actions_equiv_dir_cond (dir: Direction) (P: leaf -> Prop) (acts1 acts2: actions): Prop :=
       forall lf, P lf ->
       forall t1 t2
         (TREE1: is_tree rer acts1 (fst lf) (snd lf) dir t1)
         (TREE2: is_tree rer acts2 (fst lf) (snd lf) dir t2),
         tree_equiv_tr_dir (fst lf) (snd lf) dir t1 t2.
-    
+
     (* Stating for all directions *)
     Definition actions_equiv (acts1 acts2: actions): Prop :=
       forall dir, actions_equiv_dir dir acts1 acts2.
@@ -64,7 +64,7 @@ Section Definitions.
     Definition tree_equiv_dir dir r1 r2 :=
       def_groups r1 = def_groups r2 /\
       actions_equiv_dir dir [Areg r1] [Areg r2].
-    
+
     (* Stating for all directions *)
     Definition tree_equiv r1 r2 :=
       forall dir, tree_equiv_dir dir r1 r2.
@@ -198,7 +198,7 @@ Section Definitions.
         | d => d
         end
       end.
-  
+
   End Contexts.
 
 
@@ -415,7 +415,7 @@ Section Relation.
         symmetry proved by actions_equiv_sym
         transitivity proved by actions_equiv_trans
         as actions_equiv_rel.
-  
+
   End Actions.
 
 
@@ -423,7 +423,7 @@ Section Relation.
 
   Section DirSpecific.
     Context (dir: Direction).
-      
+
     (* tree_equiv_dir *)
     Lemma tree_equiv_dir_reflexive:
       Relation_Definitions.reflexive regex (tree_equiv_dir rer dir).
@@ -515,7 +515,7 @@ Section Relation.
       symmetry proved by tree_equiv_symmetric
       transitivity proved by tree_equiv_transitive
       as tree_equiv_rel.
-      
+
 
   (* tree_equiv_compute *)
   Lemma tree_equiv_compute_reflexive:
@@ -563,7 +563,7 @@ Section Relation.
         tree_equiv_rw. destruct H as [i [gm H]]. exists i. exists gm.
         symmetry. auto.
       Qed.
-      
+
       #[global] Add Relation regex (tree_nequiv_dir rer dir)
           symmetry proved by tree_nequiv_dir_sym
           as tree_nequiv_dir_rel.
@@ -595,14 +595,14 @@ Section Relation.
       pose proof tree_nequiv_dir_irrefl. unfold Irreflexive, Reflexive, complement in H0.
       eauto.
     Qed.
-    
+
     Lemma tree_nequiv_sym:
       Relation_Definitions.symmetric regex (tree_nequiv rer).
     Proof.
       unfold Relation_Definitions.symmetric, tree_nequiv. intros x y [dir H].
       exists dir. symmetry. auto.
     Qed.
-      
+
     #[global] Add Relation regex (tree_nequiv rer)
         symmetry proved by tree_nequiv_sym
         as tree_nequiv_rel.
@@ -689,19 +689,19 @@ Section Congruence.
     induction TREE_1; intros; simpl in *.
     - (* Done *)
       rewrite <- app_nil_r. constructor; constructor. auto.
-    
+
     - (* Check pass *)
       inversion TREE_APP; subst. 2: contradiction.
       simpl. apply IHTREE_1. auto.
-    
+
     - (* Check fail *)
       inversion TREE_APP; subst. 1: contradiction.
       simpl. constructor.
-    
+
     - (* Close *)
       inversion TREE_APP; subst. simpl.
       apply IHTREE_1. auto.
-    
+
     - (* Epsilon *)
       inversion TREE_APP; subst. auto.
 
@@ -712,28 +712,28 @@ Section Congruence.
       rewrite advance_input_success with (nexti := nextinp).
       2: eauto using read_char_success_advance.
       auto.
-    
+
     - (* Read char fail *)
       inversion TREE_APP; subst. 1: congruence.
       simpl. constructor.
-    
+
     - (* Disjunction *)
       inversion TREE_APP; subst.
       simpl. apply FlatMap_app; auto.
-    
+
     - (* Sequence *)
       inversion TREE_APP; subst.
       rewrite app_assoc in CONT. auto.
-    
+
     - (* Forced quantifier *)
       inversion TREE_APP; subst. simpl.
       auto.
-    
+
     - (* Done quantifier *)
       inversion TREE_APP; subst.
       2: { destruct plus; discriminate. }
       auto.
-    
+
     - (* Free quantifier *)
       inversion TREE_APP; subst.
       1: { destruct plus; discriminate. }
@@ -747,11 +747,11 @@ Section Congruence.
         simpl. apply FlatMap_app; auto.
       + (* Lazy *)
         simpl. apply FlatMap_app; auto.
-      
+
     - (* Group *)
       inversion TREE_APP; subst. simpl.
       auto.
-    
+
     - (* Lookaround success *)
       inversion TREE_APP; subst;
         assert (treelk0 = treelk) by (eapply is_tree_determ; eauto); subst.
@@ -771,23 +771,23 @@ Section Congruence.
         { apply leaves_group_map_indep with (gm1 := gmlk) (inp1 := inp) (dir1 := lk_dir lk).
           apply hd_error_none_nil. rewrite <- first_tree_leaf. auto. }
         simpl. rewrite Hpos, H. auto.
-  
+
     - (* Lookaround failure *)
       inversion TREE_APP; subst;
         assert (treelk0 = treelk) by (eapply is_tree_determ; eauto); subst.
       { rewrite RES_LK in FAIL_LK. inversion FAIL_LK. }
       simpl. constructor.
-    
+
     - (* Anchor *)
       inversion TREE_APP; subst.
       2: congruence.
       simpl. auto.
-    
+
     - (* Anchor fail *)
       inversion TREE_APP; subst.
       1: congruence.
       simpl. constructor.
-    
+
     - (* Backref *)
       inversion TREE_APP; subst.
       2: congruence.
@@ -796,7 +796,7 @@ Section Congruence.
       replace (advance_input_n _ _ _) with nextinp.
       2: eauto using read_backref_success_advance.
       auto.
-    
+
     - (* Backref fail *)
       inversion TREE_APP; subst.
       1: congruence.
@@ -843,7 +843,7 @@ Section Congruence.
     eauto using flatmap_leaves_equiv_l, act_from_leaf_determ.
   Qed.
 
-  
+
   (* Same as app_eq_right, but prepending this time the actions to the left *)
   (* Used in the sequence case *)
   Lemma app_eq_left:
@@ -864,7 +864,7 @@ Section Congruence.
     unfold equiv_leaffuncts. intros lf yf yg Hyf Hyg.
     inversion Hyf; subst. inversion Hyg; subst. apply ACTS_EQ; auto.
   Qed.
-  
+
   (* If a1 ≅ a2 and b1 ≅ b2, then a1 ++ b1 ≅ a2 ++ b2. *)
   (* Used in quantifier case of contextual equivalence proof *)
   Lemma app_eq_both:
@@ -1064,12 +1064,12 @@ Section Congruence.
     - (* Forward *)
       apply StrictSuffix.ss_fwd_diff in STRICT_SUFFIX.
       destruct STRICT_SUFFIX as [diff [DIFF_NOTNIL [Heqnext2 Heqpref1]]]. simpl.
-      rewrite Heqnext2, app_length.
+      rewrite Heqnext2, length_app.
       destruct diff; try contradiction. simpl. lia.
     - (* Backward *)
       apply StrictSuffix.ss_bwd_diff in STRICT_SUFFIX.
       destruct STRICT_SUFFIX as [diff [DIFF_NOTNIL [Heqnext1 Heqpref2]]]. simpl.
-      rewrite Heqpref2, app_length, rev_length.
+      rewrite Heqpref2, length_app, length_rev.
       destruct diff; try contradiction. simpl. lia.
   Qed.
 
@@ -1203,7 +1203,7 @@ Section Congruence.
       unfold tree_equiv_tr_dir in *.
       simpl. apply leaves_equiv_app; auto.
       assert (t1 = t0) by (eapply is_tree_determ; eauto). subst t1. apply leaves_equiv_refl.
-    
+
     - (* Disjunction right *)
       simpl in *. unfold tree_equiv_dir, actions_equiv_dir in *. specialize (IHctx Hctxdir).
       destruct IHctx as [IHgroups IHctx]. split.
@@ -1227,7 +1227,7 @@ Section Congruence.
       + (* Backward *)
         simpl in *. pose proof app_eq_right _ _ [Areg r0] backward IHctx.
         unfold actions_equiv_dir in H. simpl in H. unfold tree_equiv_tr_dir in *. auto.
-      
+
     - (* Sequence right *)
       simpl in *. unfold tree_equiv_dir, actions_equiv_dir in *. specialize (IHctx Hctxdir).
       destruct IHctx as [IHgroups IHctx]. split.
@@ -1241,7 +1241,7 @@ Section Congruence.
       + (* Backward *)
         simpl in *. pose proof app_eq_left _ _ [Areg r0] backward IHctx.
         unfold actions_equiv_dir in H. simpl in H. unfold tree_equiv_tr_dir in *. auto.
-      
+
     - (* Quantified *)
       simpl in *. specialize (IHctx Hctxdir). apply regex_equiv_quant. auto.
 
@@ -1330,7 +1330,7 @@ Section Congruence.
     intros ctx H. simpl in *.
     destruct (ctx_dir ctx); try discriminate; auto.
   Qed.
-  
+
   Lemma ctx_dir_lookahead_bwd_inv:
     forall ctx,
       ctx_dir (CLookaround LookAhead ctx) = Backward ->
@@ -1366,7 +1366,7 @@ Section Congruence.
     intros ctx H. simpl in *.
     destruct (ctx_dir ctx); try discriminate; auto.
   Qed.
-  
+
   Lemma ctx_dir_neglookahead_bwd_inv:
     forall ctx,
       ctx_dir (CLookaround NegLookAhead ctx) = Backward ->
diff --git a/Rewriting/FlatMap.v b/Rewriting/FlatMap.v
index c8c0290..078e003 100644
--- a/Rewriting/FlatMap.v
+++ b/Rewriting/FlatMap.v
@@ -1,5 +1,5 @@
 From Linden Require Import LeavesEquivalence Parameters Tree.
-From Coq Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 
diff --git a/Rewriting/LeavesEquivalence.v b/Rewriting/LeavesEquivalence.v
index b3bfb11..6454e27 100644
--- a/Rewriting/LeavesEquivalence.v
+++ b/Rewriting/LeavesEquivalence.v
@@ -1,6 +1,6 @@
 From Linden Require Import Parameters Groups Chars Tree.
 From Warblre Require Import RegExpRecord Typeclasses.
-From Coq Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 (** * Equivalence of lists of leaves: definition and lemmas *)
diff --git a/Rewriting/ProofSetup.v b/Rewriting/ProofSetup.v
index 9b5b3b2..5f24182 100644
--- a/Rewriting/ProofSetup.v
+++ b/Rewriting/ProofSetup.v
@@ -1,7 +1,7 @@
 (** * Importing this module will bring into the context definitions, theorems and
 tactics useful to perform rewriting proofs. *)
 
-From Coq Require Export List Lia.
+From Stdlib Require Export List Lia.
 From Warblre Require Export Base RegExpRecord.
 From Linden Require Export Regex Chars Groups Tree Semantics FunctionalSemantics FunctionalUtils ComputeIsTree.
 From Linden Require Export Parameters.
diff --git a/Semantics/Chars.v b/Semantics/Chars.v
index b1ed530..cdc1d5a 100644
--- a/Semantics/Chars.v
+++ b/Semantics/Chars.v
@@ -1,4 +1,4 @@
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 From Linden Require Import Utils Parameters LWParameters.
 Import Utils.List.
@@ -127,11 +127,11 @@ Section Chars.
       CharSet.exist_canonicalized rer Characters.all c
     else
       CharSet.exist_canonicalized rer (CharSet.remove_all Characters.all Characters.line_terminators) c.
-  
+
   Fixpoint char_match' (ccan: Character) (cd: char_descr): bool :=
     match cd with
     | CdEmpty => false
-    | CdDot => 
+    | CdDot =>
         dot_matches (RegExpRecord.dotAll rer) ccan
     | CdAll => true
     | CdSingle c' => ccan == Character.canonicalize rer c'
diff --git a/Semantics/ComputeIsTree.v b/Semantics/ComputeIsTree.v
index dd3313a..e7c67c1 100644
--- a/Semantics/ComputeIsTree.v
+++ b/Semantics/ComputeIsTree.v
@@ -1,6 +1,6 @@
 From Linden Require Import Semantics FunctionalSemantics Chars StrictSuffix Parameters.
 From Warblre Require Import Parameters Base RegExpRecord.
-From Coq Require Import Lia List.
+From Stdlib Require Import Lia List.
 
 (** * Proving that the functional version of the semantics, compute_tree,
 yields trees that respect the inductive semantics *)
@@ -18,7 +18,7 @@ Section ComputeIsTree.
 
     intros act inp gm dir t. simpl.
     destruct act as [|[reg | inpcheck | gid] acts].
-    1: { 
+    1: {
       intros H. injection H as <-. apply tree_match.
     }
 
@@ -26,7 +26,7 @@ Section ComputeIsTree.
 
     - (* Empty *)
       intros H. apply tree_epsilon. apply IHfuel; auto.
-    
+
     - (* Char *)
       destruct Chars.read_char as [[c nextinp]|] eqn:Hreadchar.
       + destruct (compute_tree rer acts nextinp gm dir fuel) as [treecont|] eqn:Hcomputecont; try discriminate.
@@ -34,16 +34,16 @@ Section ComputeIsTree.
         apply tree_char with (nextinp := nextinp); auto.
       + intros H. injection H as <-.
         apply tree_char_fail. auto.
-    
+
     - (* Disjunction *)
       destruct compute_tree as [t1|] eqn:Hcompute1; try discriminate.
       destruct (compute_tree rer (Areg r2 :: acts)%list inp gm dir fuel) as [t2|] eqn:Hcompute2; try discriminate.
       intros H. injection H as <-.
       apply tree_disj; apply IHfuel; auto.
-    
+
     - (* Sequence *)
       intros Hcompsucc. apply tree_sequence; apply IHfuel; auto.
-    
+
     - (* Quantified *)
       destruct min as [|min'].
       1: destruct delta as [[|n']|].
@@ -74,7 +74,7 @@ Section ComputeIsTree.
         destruct compute_tree as [titer|] eqn:Hiter; simpl; try discriminate.
         intros H. injection H as <-.
         apply tree_quant_forced; auto.
-    
+
     - (* Lookaround *)
       destruct compute_tree as [treelk|] eqn:Htreelk; simpl; try discriminate.
       destruct (lk_result lk treelk gm inp) eqn:LKRES.
@@ -100,7 +100,7 @@ Section ComputeIsTree.
       + (* Anchor is not satisfied *)
         intros H. injection H as <-.
         apply tree_anchor_fail; auto.
-    
+
     - (* Backreference *)
       destruct read_backref as [[br_str nextinp]|] eqn:Hreadbr.
       + (* Success *)
@@ -110,7 +110,7 @@ Section ComputeIsTree.
       + (* Failure *)
         intro H. injection H as <-.
         auto using tree_backref_fail.
-    
+
     - (* Check *)
       destruct is_strict_suffix eqn:Hssuffix.
       + (* Is strict suffix *)
diff --git a/Semantics/Examples.v b/Semantics/Examples.v
index ecd7890..4398099 100644
--- a/Semantics/Examples.v
+++ b/Semantics/Examples.v
@@ -1,6 +1,6 @@
 (** * Some examples of Backtracking Trees  *)
 
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups.
@@ -9,7 +9,7 @@ From Warblre Require Import Base RegExpRecord.
 From Linden Require Import FunctionalUtils FunctionalSemantics.
 From Linden Require Import Inst.
 From Warblre Require Import Inst.
-Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Stdlib.Strings.Ascii Stdlib.Strings.String.
 Open Scope string_scope.
 
 
@@ -40,7 +40,7 @@ Example fig2_regex: regex :=
           a_char))
     (Sequence b_char c_char).
 
-Example fig2_input: input := Input [a;b;b;c] []. 
+Example fig2_input: input := Input [a;b;b;c] [].
 
 Example fig2_tree: tree :=
   Choice
diff --git a/Semantics/FunctionalSemantics.v b/Semantics/FunctionalSemantics.v
index 211f2f8..d2d18c6 100644
--- a/Semantics/FunctionalSemantics.v
+++ b/Semantics/FunctionalSemantics.v
@@ -1,4 +1,4 @@
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 From Linden Require Import Regex Chars.
@@ -9,7 +9,7 @@ From Linden Require Import StrictSuffix.
 From Linden Require Import Parameters.
 From Warblre Require Import Numeric Base RegExpRecord.
 
-From Coq Require Import Lia DecidableClass.
+From Stdlib Require Import Lia DecidableClass.
 
 (** * Functional version of the inductive semantics *)
 
@@ -327,7 +327,7 @@ Section FunctionalSemantics.
   Proof.
     intros n l x q Hskipn.
     pose proof firstn_skipn n l. rewrite Hskipn in H.
-    pose proof skipn_length n l. rewrite Hskipn in H0.
+    pose proof length_skipn n l. rewrite Hskipn in H0.
     simpl in H0. lia.
   Qed.
 
@@ -342,7 +342,7 @@ Section FunctionalSemantics.
       destruct (skipn n next) as [|h next'] eqn:Hskipn; try discriminate.
       injection Hadv as <-.
       pose proof firstn_skipn n next. rewrite Hskipn in H. rewrite <- H.
-      pose proof skipn_length n next. rewrite Hskipn in H0.
+      pose proof length_skipn n next. rewrite Hskipn in H0.
       assert (Hlen: length (firstn n next) = n). {
         simpl in *.
         assert (length next > n) by lia.
@@ -360,7 +360,7 @@ Section FunctionalSemantics.
       destruct (skipn n pref) as [|h pref'] eqn:Hskipn; try discriminate.
       injection Hadv as <-.
       pose proof firstn_skipn n pref. rewrite Hskipn in H. rewrite <- H.
-      pose proof skipn_length n pref. rewrite Hskipn in H0.
+      pose proof length_skipn n pref. rewrite Hskipn in H0.
       assert (Hlen: length (firstn n pref) = n). {
         simpl in *.
         assert (length pref > n) by lia.
@@ -382,7 +382,7 @@ Section FunctionalSemantics.
   Proof.
     intros n l Hskipn.
     pose proof firstn_skipn n l. rewrite Hskipn in H.
-    apply (f_equal (length (A := A))) in H. rewrite app_length in H.
+    apply (f_equal (length (A := A))) in H. rewrite length_app in H.
     simpl in H. rewrite <- plus_n_O in H. rewrite <- H. apply firstn_le_length.
   Qed.
 
@@ -470,7 +470,7 @@ Section FunctionalSemantics.
   Fixpoint compute_tree (act: actions) (inp: input) (gm: group_map) (dir: Direction) (fuel:nat): option tree :=
     match fuel with
     | 0 => None
-    | S fuel => 
+    | S fuel =>
         match act with
         (* tree_done *)
         | [] => Some Match
@@ -481,13 +481,13 @@ Section FunctionalSemantics.
               | Some treecont => Some (Progress treecont)
               | None => None
               end
-            else Some Mismatch            
+            else Some Mismatch
         (* tree_close *)
         | Aclose gid :: cont =>
             match (compute_tree cont inp (GroupMap.close (idx inp) gid gm) dir fuel) with
             | Some treecont => Some (GroupAction (Close gid) treecont)
             | None => None
-            end          
+            end
         (* tree_epsilon *)
         | Areg Epsilon::cont => compute_tree cont inp gm dir fuel
         (* tree_char, tree_char_fail *)
@@ -515,7 +515,7 @@ Section FunctionalSemantics.
             match compute_tree (Areg r1 :: Areg (Quantified greedy min delta r1) :: cont) inp (GroupMap.reset gidl gm) dir fuel with
             | Some titer => Some (GroupAction (Reset gidl) titer)
             | None => None
-            end          
+            end
         (* tree_quant_done *)
         | Areg (Quantified greedy 0 (NoI.N 0) r1)::cont =>
             compute_tree cont inp gm dir fuel
@@ -531,7 +531,7 @@ Section FunctionalSemantics.
             match compute_tree (Areg r1 :: Aclose gid :: cont) inp (GroupMap.open (idx inp) gid gm) dir fuel with
             | Some treecont => Some (GroupAction (Open gid) treecont)
             | _ => None
-            end          
+            end
         (* tree_lk, tree_lk_fail *)
         | Areg (Lookaround lk r1)::cont =>
             let treelk := compute_tree [Areg r1] inp gm (lk_dir lk) fuel in
@@ -569,7 +569,7 @@ Section FunctionalSemantics.
           end
         end
     end.
-    
+
   (** * Functional Semantics Termination  *)
 
   Lemma somenone:
@@ -594,7 +594,7 @@ Section FunctionalSemantics.
       compute_tree act inp gm dir fuel <> None.
   Proof.
     intros act inp gm dir fuel H.
-    generalize dependent act. generalize dependent inp. 
+    generalize dependent act. generalize dependent inp.
     generalize dependent gm. generalize dependent dir.
     induction fuel; intros.
     { inversion H. }
@@ -675,7 +675,7 @@ Section FunctionalSemantics.
         assert (ENOUGH: fuel > actions_fuel act inp dir). { pose proof anchor_termination act inp dir a. lia. }
         apply IHfuel with (gm := gm) in ENOUGH.
         destruct compute_tree; [apply somenone|contradiction].
-      + simpl.    (* Backreferences *) 
+      + simpl.    (* Backreferences *)
         destruct read_backref as [[br_str nextinp]|] eqn:Hreadbr; try apply somenone.
         apply backref_termination with (cont := act) in Hreadbr.
         assert (ENOUGH: fuel > actions_fuel act nextinp dir) by lia.
diff --git a/Semantics/FunctionalUtils.v b/Semantics/FunctionalUtils.v
index 0f8d06a..6bcdfb4 100644
--- a/Semantics/FunctionalUtils.v
+++ b/Semantics/FunctionalUtils.v
@@ -1,4 +1,4 @@
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Warblre Require Import Base RegExpRecord.
 From Linden Require Import Regex Chars Groups Tree Semantics FunctionalSemantics ComputeIsTree Parameters.
 Import ListNotations.
diff --git a/Semantics/GroupMapLemmas.v b/Semantics/GroupMapLemmas.v
index 5a1051b..84a15a4 100644
--- a/Semantics/GroupMapLemmas.v
+++ b/Semantics/GroupMapLemmas.v
@@ -1,5 +1,5 @@
 From Linden Require Import Groups Tactics.
-From Coq Require Import List DecidableClass Lia PeanoNat.
+From Stdlib Require Import List DecidableClass Lia PeanoNat.
 
 (** * Lemmas related to group maps *)
 
diff --git a/Semantics/Groups.v b/Semantics/Groups.v
index 97bd897..2c28f0d 100644
--- a/Semantics/Groups.v
+++ b/Semantics/Groups.v
@@ -1,9 +1,9 @@
 (* Defining Capture Group Registers *)
 (* Keeping an index of when a group was opened and closed *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
-Require Import MSetList OrdersAlt PeanoNat FMapList.
+From Stdlib Require Import MSetList OrdersAlt PeanoNat FMapList.
 
 From Linden Require Import Chars.
 From Warblre Require Import Typeclasses.
diff --git a/Semantics/Parameters.v b/Semantics/Parameters.v
index c0cecbb..5c8db90 100644
--- a/Semantics/Parameters.v
+++ b/Semantics/Parameters.v
@@ -1,5 +1,5 @@
 From Warblre Require Import Parameters RegExpRecord.
-From Coq Require Import List.
+From Stdlib Require Import List.
 
 (** * Typeclass containing parameters which our development depends on *)
 
diff --git a/Semantics/Regex.v b/Semantics/Regex.v
index bfd75ff..2c9f6a4 100644
--- a/Semantics/Regex.v
+++ b/Semantics/Regex.v
@@ -1,4 +1,4 @@
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 From Linden Require Import Chars.
@@ -43,12 +43,12 @@ Inductive anchor: Type :=
 
 Section Regex.
   Context {params: LindenParameters}.
-  
+
   (** * Regex Syntax  *)
   Inductive regex : Type :=
-  | Epsilon 
+  | Epsilon
   | Character (cd : char_descr)   (* includes character classes and dot *)
-  | Disjunction (r1 r2 : regex) 
+  | Disjunction (r1 r2 : regex)
   | Sequence (r1 r2 : regex)
   | Quantified (greedy:bool) (min: nat) (delta: non_neg_integer_or_inf) (r1: regex) (* means any number of repetitions of r1 between min and min+delta *)
   | Lookaround (lk: lookaround) (r: regex)
@@ -134,5 +134,5 @@ Section Regex.
   (* r?? *)
   Definition lazy_qmark (r:regex) : regex :=
     Quantified false 0 (NoI.N 1) r.
-  
+
 End Regex.
diff --git a/Semantics/Semantics.v b/Semantics/Semantics.v
index 61240e3..24eb605 100644
--- a/Semantics/Semantics.v
+++ b/Semantics/Semantics.v
@@ -1,4 +1,4 @@
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 From Linden Require Import Regex Chars.
@@ -8,7 +8,7 @@ From Warblre Require Import Numeric Base RegExpRecord.
 From Linden Require Import Groups.
 From Linden Require Import StrictSuffix.
 From Linden Require Import Parameters LWParameters.
-From Coq Require Import Lia.
+From Stdlib Require Import Lia.
 
 (** * Inductive semantics of JavaScript regexes *)
 (* This relates a regex and a string to their backtracking tree *)
@@ -49,7 +49,7 @@ Section Semantics.
         end
       end
     end.
-  
+
   Lemma read_backref_success_advance:
     forall gm gid inp dir br_str nextinp,
       read_backref gm gid inp dir = Some (br_str, nextinp) ->
@@ -67,7 +67,7 @@ Section Semantics.
         rewrite EqDec.inversion_true in Hsubeq.
         replace (length br_str) with (endIdx - startIdx). 1: reflexivity.
         rewrite <- H. apply (f_equal (length (A := Parameters.Character))) in Hsubeq.
-        do 2 rewrite map_length in Hsubeq. rewrite firstn_length. lia.
+        do 2 rewrite length_map in Hsubeq. rewrite length_firstn. lia.
       + (* Backward *)
         destruct Nat.leb eqn:Hinb; try discriminate.
         rewrite PeanoNat.Nat.leb_gt in Hinb.
@@ -76,7 +76,7 @@ Section Semantics.
         rewrite EqDec.inversion_true in Hsubeq.
         replace (length br_str) with (endIdx - startIdx). 1: reflexivity.
         rewrite <- H. apply (f_equal (length (A := Parameters.Character))) in Hsubeq.
-        do 2 rewrite map_length in Hsubeq. rewrite rev_length, firstn_length. lia.
+        do 2 rewrite length_map in Hsubeq. rewrite length_rev, length_firstn. lia.
     - injection H as <- <-. simpl. now destruct inp, dir.
     - injection H as <- <-. simpl. now destruct inp, dir.
   Qed.
diff --git a/Semantics/StrictSuffix.v b/Semantics/StrictSuffix.v
index 645ae70..8f69721 100644
--- a/Semantics/StrictSuffix.v
+++ b/Semantics/StrictSuffix.v
@@ -1,6 +1,6 @@
 From Linden Require Import Chars Parameters LWParameters.
 From Warblre Require Import Base Parameters.
-From Coq Require Import List Lia.
+From Stdlib Require Import List Lia.
 Import ListNotations.
 
 
@@ -99,7 +99,7 @@ Section StrictSuffix.
           apply ss_next with (inp2 := Input (a::next1) (rev (x :: diff'') ++ pref2)).
           * simpl. f_equal. f_equal. rewrite Hpref12. simpl.
             rewrite rev_app_distr, <- app_assoc, <- app_assoc, <- app_assoc. reflexivity.
-          * simpl in *. rewrite app_length in Hlendiff. simpl in *. apply IH with (diff := x :: diff'').
+          * simpl in *. rewrite length_app in Hlendiff. simpl in *. apply IH with (diff := x :: diff'').
             -- simpl. lia.
             -- lia.
             -- rewrite <- app_comm_cons. rewrite <- app_assoc in Hnext12. auto.
@@ -144,8 +144,8 @@ Section StrictSuffix.
           apply ss_next with (inp2 := Input (diff'' ++ a :: next2) (x :: pref1)).
           * simpl. f_equal. f_equal. rewrite Hnext12. simpl.
             rewrite <- app_assoc. reflexivity.
-          * simpl in *. rewrite app_length in Hlendiff. simpl in *. apply IH with (diff := diff'' ++ [a]).
-            -- rewrite app_length. simpl. lia.
+          * simpl in *. rewrite length_app in Hlendiff. simpl in *. apply IH with (diff := diff'' ++ [a]).
+            -- rewrite length_app. simpl. lia.
             -- lia.
             -- rewrite <- app_assoc. auto.
             -- rewrite <- app_assoc in Hpref12. auto.
diff --git a/Semantics/Tree.v b/Semantics/Tree.v
index 13c1bcc..78944f9 100644
--- a/Semantics/Tree.v
+++ b/Semantics/Tree.v
@@ -1,8 +1,8 @@
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 From Linden Require Import Regex Chars Groups Parameters LWParameters.
-From Coq Require Import PeanoNat.
+From Stdlib Require Import PeanoNat.
 From Warblre Require Import Typeclasses Parameters Base.
 
 (** * Backtracking trees *)
@@ -34,7 +34,7 @@ Proof. intros X Y l. induction l; intros; simpl; auto. Qed.
 
 Lemma seqop_list_head_some:
   forall X Y (h:X) l f (r:Y),
-    f h = Some r -> 
+    f h = Some r ->
     seqop_list (h::l) f = Some r.
 Proof.
   intros X Y h l f r H. unfold seqop_list.
@@ -44,7 +44,7 @@ Qed.
 
 Lemma seqop_list_head_none:
   forall X Y (h:X) l (f:X -> option Y),
-    f h = None -> 
+    f h = None ->
     seqop_list (h::l) f = seqop_list l f.
 Proof. intros. unfold seqop_list. simpl. rewrite H. auto. Qed.
 
@@ -64,7 +64,7 @@ Definition option_flat_map {A B: Type} (f: A -> option B) (o: option A) : option
 
 Section Tree.
   Context {params: LindenParameters}.
-  
+
   Inductive tree : Type :=
   | Mismatch
   | Match
@@ -87,7 +87,7 @@ Section Tree.
 
   Definition tree_eqb (t1 t2:tree) : bool :=
   match tree_eq_dec t1 t2 with | left _ => true | _ => false end.
-  
+
   (** ** Maximum group ID of a tree *)
   (* Maximum group ID of a list of group IDs *)
   Fixpoint max_gid_list (gl: list group_id) :=
@@ -153,7 +153,7 @@ Section Tree.
     | GroupAction a t1 => tree_res t1 (GroupMap.update (idx inp) a gm) inp dir
     | LK lk tlk t1 =>
         match (positivity lk) with
-        | true => 
+        | true =>
             match tree_res tlk gm inp (lk_dir lk) with
             | None => None
             (* using the captures defined in the first branch of the lookahead *)
diff --git a/Utils/CanonicalMaps.v b/Utils/CanonicalMaps.v
index 15e8179..e9f84c4 100644
--- a/Utils/CanonicalMaps.v
+++ b/Utils/CanonicalMaps.v
@@ -1,4 +1,4 @@
-From Coq Require Import Eqdep_dec List Permutation SetoidList Bool RelationClasses.
+From Stdlib Require Import Eqdep_dec List Permutation SetoidList Bool RelationClasses.
 
 (** Canonical maps *)
 (* Maps for which for all maps m1 and m2, we have Equal m1 m2 <-> m1 = m2. *)
@@ -146,7 +146,7 @@ Proof.
   - intros * ->%Hl _ ->; reflexivity.
 Qed.
 
-Require Import FMapInterface FMapList FMapFacts.
+From Stdlib Require Import FMapInterface FMapList FMapFacts.
 
 Module Type OrderedTypeWithIrrelevance.
   Declare Module OT: OrderedType.
diff --git a/WarblreEquiv/CharDescrCharSet.v b/WarblreEquiv/CharDescrCharSet.v
index fac603a..cb0c451 100644
--- a/WarblreEquiv/CharDescrCharSet.v
+++ b/WarblreEquiv/CharDescrCharSet.v
@@ -2,7 +2,7 @@ From Linden Require Import Chars LWParameters Parameters RegexpTranslation Warbl
 From Warblre Require Import Parameters Semantics Result Patterns RegExpRecord Typeclasses.
 Import Result.Notations.
 Import Patterns.
-From Coq Require Import Lia.
+From Stdlib Require Import Lia.
 
 Local Open Scope result_flow.
 
@@ -11,7 +11,7 @@ Local Open Scope result_flow.
 Section CharDescrCharSet.
   Context {params: LindenParameters}.
   Context (rer: RegExpRecord).
-  
+
   (* Definition *)
   Definition equiv_cd_charset (cd: char_descr) (charset: CharSet) :=
     forall c: Character, char_match rer c cd = CharSet.exist_canonicalized rer charset (Character.canonicalize rer c).
@@ -99,7 +99,7 @@ Section CharDescrCharSet.
     intros HnoDotAll c. unfold char_match. simpl. unfold dot_matches. rewrite HnoDotAll.
     reflexivity.
   Qed.
-    
+
   Lemma equiv_cd_single:
     forall c, equiv_cd_charset (CdSingle c) (CharSet.singleton c).
   Proof.
diff --git a/WarblreEquiv/Equiv.v b/WarblreEquiv/Equiv.v
index 94ef09a..6ad5584 100644
--- a/WarblreEquiv/Equiv.v
+++ b/WarblreEquiv/Equiv.v
@@ -9,7 +9,7 @@ Import Result.Notations.
 Import Notation.
 Import NodeProps.Zipper.
 Import Match.
-From Coq Require Import ZArith PeanoNat Lia RelationClasses.
+From Stdlib Require Import ZArith PeanoNat Lia RelationClasses.
 
 Local Open Scope result_flow.
 
@@ -120,7 +120,7 @@ Section Equiv.
 
       (* About mc ms *)
       unfold equiv_cont in Hequivcont. specialize (Hequivcont gm ms inp).
-      
+
       (* Deduplicate Linden part *)
       set (topt := (match compute_tree rer _ inp _ dir fueltree with | Some titer => _ | None => None end)).
       replace (match delta with | NoI.N n => _ | +∞ => _ end) with topt.
@@ -151,7 +151,7 @@ Section Equiv.
         destruct resloop as [resloopms|]; simpl in *.
         + injection Hres as <-. inversion Hequiv. simpl. unfold gmreset in H. rewrite <- H. simpl. constructor; assumption.
         + inversion Hequiv. simpl. unfold gmreset in H0. rewrite <- H0. simpl. eapply Hequivcont; eauto using ms_valid_wrt_checks_tail.
-      
+
       - destruct (mc ms) as [resskip|] eqn:Hresskipsucc; simpl; try discriminate.
         (* Probably similar to greedy case *)
         specialize (Hequivcont resskip fueltree tskip Hinpcompat Hgmms Hgmgl Hmsinp).
@@ -426,7 +426,7 @@ Section Equiv.
              unfold equiv_cont in Hequivcont.
              (*rewrite <- Hfirstn_next_substr.*)
              replace (length (List.firstn _ next)) with (Z.to_nat rlen).
-             2: { symmetry in Hoobiff. rewrite Nat.leb_gt in Hoobiff. rewrite List.firstn_length. lia. }
+             2: { symmetry in Hoobiff. rewrite Nat.leb_gt in Hoobiff. rewrite List.length_firstn. lia. }
              fold inp'.
              apply Hequivcont with (ms := ms') (fuel := fuel); auto.
              (* Remains to prove that the new MatchState remains valid with respect to the checks in act *)
@@ -435,7 +435,7 @@ Section Equiv.
              specialize (Hmschecks inpcheck Hcheckin). inversion Hmschecks as [ms0 inpcheck0 Hendge |]. subst ms0 inpcheck0.
              constructor.
              assert (MatchState.endIndex ms' >= MatchState.endIndex ms)%Z. {
-               unfold ms', endMatch. simpl. lia. 
+               unfold ms', endMatch. simpl. lia.
              }
              lia.
       + (* Backward *)
@@ -483,7 +483,7 @@ Section Equiv.
              intro H. injection H as <-. simpl.
              unfold equiv_cont in Hequivcont.
              replace (length (List.rev _)) with (Z.to_nat rlen).
-             2: { symmetry in Hoobiff. rewrite Nat.leb_gt in Hoobiff. rewrite List.rev_length, List.firstn_length. lia. }
+             2: { symmetry in Hoobiff. rewrite Nat.leb_gt in Hoobiff. rewrite List.length_rev, List.length_firstn. lia. }
              fold inp'.
              apply Hequivcont with (ms := ms') (fuel := fuel); auto.
              (* Remains to prove that the new MatchState remains valid with respect to the checks in act *)
@@ -492,7 +492,7 @@ Section Equiv.
              specialize (Hmschecks inpcheck Hcheckin). inversion Hmschecks as [|ms0 inpcheck0 Hendge]. subst ms0 inpcheck0.
              constructor.
              assert (MatchState.endIndex ms' <= MatchState.endIndex ms)%Z. {
-               unfold ms'. simpl. lia. 
+               unfold ms'. simpl. lia.
              }
              lia.
     - (* Range is undefined *)
@@ -608,12 +608,12 @@ Section Equiv.
       simpl.
       intro Hsubtreesucc.
       eapply Hequivcont; eauto using ms_valid_wrt_checks_tail.
-  
+
     - (* Character *)
       intros ctx Hroot Heqn Heqnm m dir Hcompsucc.
       injection Hcompsucc as <-.
       apply charSetMatcher_equiv with (inv := false); auto. apply equiv_cd_single.
-    
+
     - (* Dot *)
       intros ctx Hroot Heqn Heqnm m dir Hcompsucc.
       injection Hcompsucc as <-.
@@ -639,15 +639,15 @@ Section Equiv.
       intro H. injection H as <-.
       rewrite <- (NonNegInt.to_positive_soundness gid gid' Hgidpos).
       auto using backref_equiv.
-    
+
     - (* AtomEsc (ACharacterClassEsc esc); idem *)
       intros ctx Hroot Heqn Heqnm m dir Hcompsucc.
       eapply characterClassEscape_equiv with (nm := nm); eauto. constructor. assumption.
-    
+
     - (* AtomEsc (ACharacterEsc esc); idem *)
       intros ctx Hroot Heqn Heqnm m dir Hcompsucc.
       eapply characterEscape_equiv; eauto.
-    
+
     - (* CharacterClass; idem *)
       intros ctx Hroot Heqn Heqnm m dir Hcompsucc.
       eapply characterClass_equiv; eauto.
@@ -878,10 +878,10 @@ Section Equiv.
         * eauto using ms_valid_wrt_checks_tail.
         * eauto using noforb_tail.
 
-      
+
     - (* Anchor *)
       intros ctx Hroot Heqn Heqnm m dir. inversion Hanchequiv as [Heqwr Heqlanchor | Heqwr Heqlanchor | Heqwr Heqlanchor | Heqwr Heqlanchor].
-      
+
       + (* Input start *)
         simpl. intro H. injection H as <-.
         unfold equiv_matcher. intros str0 mc gl forbgroups act Hequivcont Hgldisj Hdef_forbid_disj.
@@ -917,7 +917,7 @@ Section Equiv.
                 simpl in *. auto. (* Copy-pasted... *)
              ++ intros H H0. injection H as <-. injection H0 as <-. simpl. constructor.
           -- intro H. injection H as <-. intro H. injection H as <-. simpl. constructor.
-      
+
       + (* Input end *)
         simpl. intro H. injection H as <-.
         unfold equiv_matcher. intros str0 mc gl forbgroups act Hequivcont Hgldisj Hdef_forbid_disj.
@@ -949,7 +949,7 @@ Section Equiv.
                 simpl in *. auto. (* Copy-pasted... *)
              ++ intros H H0. injection H as <-. injection H0 as <-. simpl. constructor.
           -- intro H. injection H as <-. intro H. injection H as <-. simpl. constructor.
-        
+
       + (* Word boundary *)
         simpl. intro H. injection H as <-.
         unfold equiv_matcher. intros str0 mc gl forbgroups act Hequivcont Hgldisj Hdef_forbid_disj.
@@ -970,7 +970,7 @@ Section Equiv.
           intro Hres. injection Hres as <-.
           unfold anchor_satisfied. destruct inp as [next pref].
           setoid_rewrite <- Hisboundary. intro H. injection H as <-. simpl. constructor.
-        
+
       + (* Non word boundary *)
         simpl. intro H. injection H as <-.
         unfold equiv_matcher. intros str0 mc gl forbgroups act Hequivcont Hgldisj Hdef_forbid_disj.
diff --git a/WarblreEquiv/EquivDef.v b/WarblreEquiv/EquivDef.v
index 7d6a983..3804f62 100644
--- a/WarblreEquiv/EquivDef.v
+++ b/WarblreEquiv/EquivDef.v
@@ -3,7 +3,7 @@ From Linden Require Import GroupMapMS MSInput GroupMapLemmas.
 From Linden Require Import LWParameters Parameters.
 From Linden Require Import Utils.
 From Warblre Require Import Parameters Notation Base Result Match RegExpRecord.
-From Coq Require Import ZArith List.
+From Stdlib Require Import ZArith List.
 Import Notation.
 Import Match.
 
diff --git a/WarblreEquiv/EquivLemmas.v b/WarblreEquiv/EquivLemmas.v
index 358e941..a5cf4fe 100644
--- a/WarblreEquiv/EquivLemmas.v
+++ b/WarblreEquiv/EquivLemmas.v
@@ -3,7 +3,7 @@ From Linden Require Import Regex GroupMapMS LWParameters Groups Tree Chars Seman
   GroupMapLemmas Tactics CharDescrCharSet LKFactorization StrictSuffix
   Parameters.
 From Warblre Require Import Parameters List Notation Result Typeclasses Base Errors RegExpRecord StaticSemantics Semantics Base.
-From Coq Require Import List ZArith Lia DecidableClass ClassicalFacts.
+From Stdlib Require Import List ZArith Lia DecidableClass ClassicalFacts.
 Import ListNotations.
 Import Notation.
 Import Result.Notations.
@@ -155,8 +155,8 @@ Section EquivLemmas.
       rewrite List.Indexing.Int.of_nat in Hreadsuccess.
       apply List.Indexing.Nat.concat in Hreadsuccess.
       destruct Hreadsuccess as [ [Habs _] | [Hzero Hreadsuccess] ].
-      1: { rewrite List.rev_length in Habs. lia. }
-      rewrite List.rev_length in Hreadsuccess.
+      1: { rewrite List.length_rev in Habs. lia. }
+      rewrite List.length_rev in Hreadsuccess.
       replace (end_ind - length pref) with 0 in Hreadsuccess by lia.
       injection Hreadsuccess as <-.
       unfold char_match. simpl.
@@ -170,11 +170,11 @@ Section EquivLemmas.
       rewrite List.Indexing.Int.of_nat in Hreadsuccess.
       apply List.Indexing.Nat.concat in Hreadsuccess.
       destruct Hreadsuccess as [ [Hlen Hreadsuccess] | [Habs _] ].
-      2: { rewrite List.app_length, List.rev_length in Habs. simpl in *. lia. }
+      2: { rewrite List.length_app, List.length_rev in Habs. simpl in *. lia. }
       injection Hlenpref as <-.
       unfold List.Indexing.Nat.indexing in Hreadsuccess.
-      rewrite List.nth_error_app2 in Hreadsuccess. 2: { rewrite List.rev_length. reflexivity. }
-      rewrite List.rev_length, Nat.sub_diag in Hreadsuccess.
+      rewrite List.nth_error_app2 in Hreadsuccess. 2: { rewrite List.length_rev. reflexivity. }
+      rewrite List.length_rev, Nat.sub_diag in Hreadsuccess.
       injection Hreadsuccess as <-.
       unfold char_match. simpl.
       setoid_rewrite char_match_warblre with (chr := chr) (cd := cd) (charset := charset); auto.
@@ -250,8 +250,8 @@ Section EquivLemmas.
       subst str0 end_ind.
       apply List.Indexing.Nat.concat in Hreadsuccess.
       destruct Hreadsuccess as [ [Habs _] | [_ Hreadsuccess] ].
-      1: { rewrite List.rev_length in Habs. lia. }
-      rewrite List.rev_length in Hreadsuccess.
+      1: { rewrite List.length_rev in Habs. lia. }
+      rewrite List.length_rev in Hreadsuccess.
       replace (length pref - length pref) with 0 in Hreadsuccess by lia.
       injection Hreadsuccess as <-.
       unfold char_match. simpl.
@@ -264,10 +264,10 @@ Section EquivLemmas.
       injection Hlenpref as <-. subst str0.
       apply List.Indexing.Nat.concat in Hreadsuccess.
       destruct Hreadsuccess as [ [Hlen Hreadsuccess] | [Habs _] ].
-      2: { rewrite List.rev_length in Habs. simpl in *. lia. }
+      2: { rewrite List.length_rev in Habs. simpl in *. lia. }
       unfold List.Indexing.Nat.indexing in Hreadsuccess. simpl in *.
-      rewrite List.nth_error_app2 in Hreadsuccess. 2: { rewrite List.rev_length. reflexivity. }
-      rewrite List.rev_length, Nat.sub_diag in Hreadsuccess.
+      rewrite List.nth_error_app2 in Hreadsuccess. 2: { rewrite List.length_rev. reflexivity. }
+      rewrite List.length_rev, Nat.sub_diag in Hreadsuccess.
       injection Hreadsuccess as <-.
       unfold char_match. simpl.
       now setoid_rewrite char_mismatch_warblre.
@@ -360,8 +360,8 @@ Section EquivLemmas.
     inversion Hmatches as [s end_ind cap next pref Hlenpref Heqs Heqms Heqinp].
     subst ms. simpl in *.
     apply (f_equal (length (A := Character))) in Heqs.
-    rewrite List.app_length in Heqs.
-    rewrite List.rev_length in Heqs.
+    rewrite List.length_app in Heqs.
+    rewrite List.length_rev in Heqs.
     assert (Hlen: end_ind = length s) by lia.
     assert (Hnext_zerolen: length next = 0) by lia.
     exists pref. f_equal.
@@ -377,7 +377,7 @@ Section EquivLemmas.
   Proof.
     intros ms [next pref] Hnotend Hmatches. destruct next as [|x next].
     - inversion Hmatches as [s end_ind cap next' pref' Hlenpref Heqs Heqms Heqinp]. subst ms next' pref'. simpl in *.
-      subst s. rewrite app_nil_r, rev_length in Hnotend. lia.
+      subst s. rewrite app_nil_r, length_rev in Hnotend. lia.
     - exists pref. exists x. exists next. reflexivity.
   Qed.
 
@@ -416,7 +416,7 @@ Section EquivLemmas.
     inversion Hmatches as [s end_ind cap next pref Hlenpref Heqs Heqms Heqinp].
     subst ms. simpl in *.
     apply (f_equal (length (A := Character))) in Heqs.
-    rewrite List.app_length, List.rev_length in Heqs.
+    rewrite List.length_app, List.length_rev in Heqs.
     assert (Hlen: end_ind = 0) by lia. subst end_ind.
     exists next. f_equal.
     now apply List.length_zero_iff_nil.
@@ -481,7 +481,7 @@ Section EquivLemmas.
     intros ms inp Hmatches.
     inversion Hmatches as [s end_ind cap next pref Hlenpref Heqs Heqms Heqinp].
     subst ms. simpl in *.
-    apply (f_equal (@length Character)) in Heqs. rewrite List.app_length, List.rev_length in Heqs.
+    apply (f_equal (@length Character)) in Heqs. rewrite List.length_app, List.length_rev in Heqs.
     subst end_ind. lia.
   Qed.
 
@@ -551,8 +551,8 @@ Section EquivLemmas.
       destruct Hinb as [_ Hinb].
       assert (Hinb': end_ind + 1 <= length s) by lia.
       apply (f_equal (length (A := Character))) in Heqs.
-      rewrite List.app_length in Heqs.
-      rewrite List.rev_length in Heqs.
+      rewrite List.length_app in Heqs.
+      rewrite List.length_rev in Heqs.
       simpl in Heqs.
       lia.
     - destruct pref as [|c pref'].
@@ -628,7 +628,7 @@ Section EquivLemmas.
       pose proof ms_matches_inp_prevchar _ _ _ Hmatches Hcl as [pref' [next0 Heqinp]]. injection Heqinp as Heqnext0 Heqpref. subst next0 pref.
       replace next with (@nil Character) in *.
       2: {
-        symmetry. apply length_zero_iff_nil. apply (f_equal (@length Character)) in Hstr0. rewrite app_length, rev_length in Hstr0. lia.
+        symmetry. apply length_zero_iff_nil. apply (f_equal (@length Character)) in Hstr0. rewrite length_app, length_rev in Hstr0. lia.
       }
       injection Hb as <-. rewrite unwrap_bool in Ha. injection Ha as <-.
       rewrite Bool.xorb_false_r. symmetry. reflexivity.
@@ -691,7 +691,7 @@ Section EquivLemmas.
     | Acheck _ :: q => actions_def_groups q
     | Aclose gid :: q => gid :: actions_def_groups q
     end.
-  
+
   (* Lemma for a list of actions *)
   Lemma actions_tree_no_outside_groups:
     forall acts gm0 inp0 dir0 fuel t,
@@ -707,7 +707,7 @@ Section EquivLemmas.
     - (* No action *)
       intro H. injection H as <-. simpl.
       intros gm1 gm2 inp1 inp2 dir H. now injection H as <- <-.
-    
+
     - (* Areg *)
       destruct reg as [ | cd | r1 r2 | r1 r2 | greedy min delta r | lk r | gid r | a | gid].
 
@@ -722,7 +722,7 @@ Section EquivLemmas.
         intro H. injection H as <-. intros gm1 gm2 inp1 inp2 dir.
         simpl. intro Hrescont. specialize (IHfuel treecont eq_refl gm1 gm2 (advance_input' inp1 dir) inp2 dir Hrescont).
         exact IHfuel.
-      
+
       + (* Disjunction *)
         destruct compute_tree as [t1|] eqn:Heqt1; simpl; try discriminate.
         destruct (compute_tree rer (Areg r2 :: acts) _ _ _ _) as [t2|] eqn:Heqt2; simpl; try discriminate.
@@ -744,7 +744,7 @@ Section EquivLemmas.
           intro Htreecomp. specialize (IHfuel (Areg r2 :: Areg r1 :: acts) gm0 inp0 backward t Htreecomp).
           simpl in IHfuel. rewrite <- app_assoc. intros. eapply IHfuel; eauto.
           do 2 rewrite in_app_iff. do 2 rewrite in_app_iff in H0. tauto.
-      
+
       + (* Quantified *)
         destruct min as [|min'].
         1: destruct (delta =? (NoI.N 0))%NoI eqn:Hdeltazero.
@@ -786,11 +786,11 @@ Section EquivLemmas.
         * (* Forced *)
           destruct compute_tree as [titer|] eqn:Hiter; try discriminate.
           intro H. injection H as <-.
-          simpl. intros gm1 gm2 inp1 inp2 dir Heqgm2 gid Hnotin. rewrite in_app_iff in Hnotin. 
+          simpl. intros gm1 gm2 inp1 inp2 dir Heqgm2 gid Hnotin. rewrite in_app_iff in Hnotin.
           rewrite (IHfuel _ _ _ _ _ Hiter _ _ _ _ _ Heqgm2).
           2: { simpl. do 2 rewrite in_app_iff. tauto. }
           assert (~In gid (def_groups r)) by tauto. now apply gm_reset_find_other.
-        
+
       + (* Lookaround *)
         destruct compute_tree as [treelk|] eqn:Hcomputelk; try discriminate.
         destruct lk_result eqn:LKRES.
@@ -820,7 +820,7 @@ Section EquivLemmas.
         2: { simpl. rewrite in_app_iff in *. simpl. tauto. }
         assert (gid <> gid') by tauto.
         now apply group_map_open_find_other.
-      
+
       + (* Anchor *)
         destruct anchor_satisfied.
         * destruct compute_tree as [treecont|] eqn:Hcomputecont; try discriminate.
@@ -832,7 +832,7 @@ Section EquivLemmas.
         * destruct compute_tree as [tcont|] eqn:Hcomputecont; try discriminate.
           intro H. injection H as <-. simpl. eauto using IHfuel.
         * intro H. injection H as <-. discriminate.
-    
+
     - (* Acheck *)
       destruct is_strict_suffix.
       + (* Check passes *)
@@ -843,7 +843,7 @@ Section EquivLemmas.
         exact IHfuel.
       + (* Check fails *)
         intro H. injection H as <-. discriminate.
-    
+
     - (* Aclose *)
       specialize (IHfuel acts (GroupMap.close (idx inp0) gid gm0) inp0 dir0).
       destruct compute_tree as [treecont|]; simpl; try discriminate.
@@ -905,7 +905,7 @@ Section EquivLemmas.
     - (* No action *)
       simpl. intros _ _ _ t H. injection H as <-. simpl.
       intros gm1 gm2 inp1 inp2 _ H. injection H as <- <-. auto.
-    
+
     - (* Epsilon *)
       simpl. intros gm0 inp dir0 t Hcomputesucc gm1 gm2 inp1 inp2 dir Heqgm2 gid idx Hopen2.
       rewrite Areg_Aclose_disappear. eauto using IHfuel.
@@ -921,7 +921,7 @@ Section EquivLemmas.
         eapply IHfuel; eauto.
       + (* Read fails *)
         intro H. injection H as <-. discriminate.
-    
+
     - (* Disjunction *)
       simpl. intros gm0 inp dir0 t.
       destruct compute_tree as [t1|] eqn:Hcompute1; try discriminate.
@@ -937,7 +937,7 @@ Section EquivLemmas.
         intros Hres2 gid idx' Hopen2.
         pose proof IHfuel _ _ _ _ _ Hcompute2 _ _ _ _ _ Hres2 _ _ Hopen2.
         simpl in H. rewrite Areg_Aclose_disappear in *. auto.
-    
+
     - (* Sequence *)
       simpl. intros gm0 inp dir0 t Hcomputesucc gm1 gm2 inp1 inp2 dir Heqgm2 gid idx' Hopen2.
       pose proof IHfuel _ _ _ _ _ Hcomputesucc _ _ _ _ _ Heqgm2 _ _ Hopen2.
@@ -1044,7 +1044,7 @@ Section EquivLemmas.
         rewrite Areg_Aclose_disappear. eauto using IHfuel.
       + (* Anchor is not satisfied *)
         intro H. injection H as <-. discriminate.
-    
+
     - (* Backreference *)
       intros gm0 inp dir t. simpl.
       destruct read_backref as [[br_str nextinp]|].
@@ -1053,7 +1053,7 @@ Section EquivLemmas.
         intros gm1 gm2 inp1 inp2 dir0 Heqgm2 gid' Hopen2.
         rewrite Areg_Aclose_disappear. eauto using IHfuel.
       + intro H. injection H as <-. discriminate.
-    
+
     - (* Check *)
       intros gm0 inp dir0 t. simpl.
       destruct is_strict_suffix.
@@ -1161,22 +1161,22 @@ Section EquivLemmas.
       + intro Habs.
         assert (next = []). {
           destruct next; try reflexivity.
-          apply (f_equal (length (A := Character))) in Habs. rewrite firstn_length in Habs. simpl in Habs. lia.
+          apply (f_equal (length (A := Character))) in Habs. rewrite length_firstn in Habs. simpl in Habs. lia.
         }
         subst next. rewrite app_nil_r in H3. rewrite <- H3 in H2.
-        apply (f_equal (length (A := Character))) in H2. rewrite app_length, rev_length, rev_length in H2. lia.
+        apply (f_equal (length (A := Character))) in H2. rewrite length_app, length_rev, length_rev in H2. lia.
       + apply (f_equal (skipn (A := Character) (length pref))) in H3, H2. rewrite skipn_app in H3, H2. rewrite <- H2 in H3.
-        rewrite rev_length, Nat.sub_diag in H3. rewrite <- rev_length in H3 at 1. rewrite skipn_all in H3.
-        simpl in *. rewrite rev_length in *. replace (length pref - length pref') with 0 in * by lia. simpl in *.
+        rewrite length_rev, Nat.sub_diag in H3. rewrite <- length_rev in H3 at 1. rewrite skipn_all in H3.
+        simpl in *. rewrite length_rev in *. replace (length pref - length pref') with 0 in * by lia. simpl in *.
         rewrite H3. f_equal.
-        rewrite firstn_app, skipn_length, rev_length, Nat.sub_diag. simpl. rewrite app_nil_r.
+        rewrite firstn_app, length_skipn, length_rev, Nat.sub_diag. simpl. rewrite app_nil_r.
         rewrite firstn_all2. 1: reflexivity.
-        rewrite skipn_length, rev_length. reflexivity.
-      + apply (f_equal (firstn (length pref'))) in H2, H3. rewrite firstn_app, rev_length in H2, H3.
-        rewrite <- rev_length in H2 at 1. rewrite firstn_all, Nat.sub_diag in H2. simpl in H2. rewrite app_nil_r in H2.
+        rewrite length_skipn, length_rev. reflexivity.
+      + apply (f_equal (firstn (length pref'))) in H2, H3. rewrite firstn_app, length_rev in H2, H3.
+        rewrite <- length_rev in H2 at 1. rewrite firstn_all, Nat.sub_diag in H2. simpl in H2. rewrite app_nil_r in H2.
         rewrite <- H2 in H3. apply (f_equal (rev (A := Character))) in H3. rewrite rev_app_distr, rev_involutive in H3.
         rewrite <- H3 at 1. f_equal.
-        rewrite firstn_all2. 2: { rewrite rev_length. lia. } apply rev_involutive.
+        rewrite firstn_all2. 2: { rewrite length_rev. lia. } apply rev_involutive.
     - (* Backward *)
       destruct inp' as [next' pref']. destruct inp as [next pref].
       apply ss_bwd_diff.
@@ -1194,22 +1194,22 @@ Section EquivLemmas.
       + intro Habs.
         assert (next' = []). {
           destruct next'; try reflexivity.
-          apply (f_equal (length (A := Character))) in Habs. rewrite firstn_length in Habs. simpl in Habs. lia.
+          apply (f_equal (length (A := Character))) in Habs. rewrite length_firstn in Habs. simpl in Habs. lia.
         }
         subst next'. rewrite app_nil_r in H2. rewrite <- H2 in H3.
-        apply (f_equal (length (A := Character))) in H3. rewrite app_length, rev_length, rev_length in H3. lia.
-      + apply (f_equal (skipn (length pref'))) in H2, H3. rewrite skipn_app, rev_length in H2, H3.
-        rewrite <- rev_length in H2 at 1. rewrite skipn_all, Nat.sub_diag in H2. simpl in H2.
+        apply (f_equal (length (A := Character))) in H3. rewrite length_app, length_rev, length_rev in H3. lia.
+      + apply (f_equal (skipn (length pref'))) in H2, H3. rewrite skipn_app, length_rev in H2, H3.
+        rewrite <- length_rev in H2 at 1. rewrite skipn_all, Nat.sub_diag in H2. simpl in H2.
         rewrite <- H2 in H3. replace (length pref' - length pref) with 0 in H3 by lia. simpl in H3.
         rewrite <- H3 at 1. f_equal.
-        rewrite <- H3. rewrite firstn_app, skipn_length, rev_length, Nat.sub_diag. simpl. rewrite app_nil_r.
+        rewrite <- H3. rewrite firstn_app, length_skipn, length_rev, Nat.sub_diag. simpl. rewrite app_nil_r.
         rewrite firstn_all2. 1: reflexivity.
-        rewrite skipn_length, rev_length. reflexivity.
-      + apply (f_equal (firstn (length pref))) in H2, H3. rewrite firstn_app, rev_length in H2, H3.
-        rewrite <- rev_length in H3 at 1. rewrite firstn_all, Nat.sub_diag in H3. simpl in H3. rewrite app_nil_r in H3.
+        rewrite length_skipn, length_rev. reflexivity.
+      + apply (f_equal (firstn (length pref))) in H2, H3. rewrite firstn_app, length_rev in H2, H3.
+        rewrite <- length_rev in H3 at 1. rewrite firstn_all, Nat.sub_diag in H3. simpl in H3. rewrite app_nil_r in H3.
         rewrite <- H3 in H2. apply (f_equal (rev (A := Character))) in H2. rewrite rev_app_distr, rev_involutive in H2.
         rewrite <- H2 at 1. f_equal.
-        rewrite firstn_all2. 2: { rewrite rev_length. lia. } apply rev_involutive.
+        rewrite firstn_all2. 2: { rewrite length_rev. lia. } apply rev_involutive.
   Qed.
 
   (* Validity wrt checks right before iterating a quantifier *)
@@ -1405,7 +1405,7 @@ Section EquivLemmas.
         unfold List.Disjoint, not in Hdef_forbid_disj. intros ->. apply Hdef_forbid_disj with (x := S n); auto. simpl. now left.
       }
       rewrite group_map_open_find_other. 2: congruence.
-      unfold no_forbidden_groups in Hnoforb. apply Hnoforb. rewrite in_app_iff. now right. 
+      unfold no_forbidden_groups in Hnoforb. apply Hnoforb. rewrite in_app_iff. now right.
   Qed.
 
   (* Lemma used when closing a group *)
@@ -1641,7 +1641,7 @@ Section EquivLemmas.
         * exfalso. apply Hgmgl in Hin. specialize (Hnoforb (S n)).
           rewrite in_app_iff in Hnoforb.
           specialize_prove Hnoforb. {
-            left. simpl. left. reflexivity. 
+            left. simpl. left. reflexivity.
           }
           congruence.
     - (* gid' is not the newly open group *)
@@ -1662,7 +1662,7 @@ Section EquivLemmas.
       (Hinp'compat: input_compat inp' str0)
       (Hgm'ms': equiv_groupmap_ms gm' ms')
       (Hgm'gl': group_map_equiv_open_groups gm' ((S n, idx inp)::gl))
-      (Heqrres: rres = 
+      (Heqrres: rres =
         if (dir ==? forward)%wt
         then
          if negb (MatchState.endIndex ms <=? MatchState.endIndex ms')%Z
@@ -1749,7 +1749,7 @@ Section EquivLemmas.
       rewrite List.Update.Nat.One.indexing_updated_other with (i := n) (ls := MatchState.captures ms') (v := r); auto.
       rewrite <- nth_indexing. apply Hgm'ms'.
   Qed.
-  
+
   Lemma equiv_open_groups_close_group:
     forall n startidx endidx gm' gl lr,
       group_map_equiv_open_groups gm' ((S n, startidx)::gl) ->
@@ -1796,7 +1796,7 @@ Section EquivLemmas.
   Proof.
     intros ms next pref rlen endMatch -> Hmsinp Hrlennneg.
     inversion Hmsinp as [str0 end_ind cap next' pref' Hlenpref Heqstr0 Heqms Heqnext']. subst next' pref' str0. simpl.
-    rewrite app_length, rev_length, Z.gtb_gt.
+    rewrite length_app, length_rev, Z.gtb_gt.
     change (match Z.to_nat rlen with | 0 => _ | S m' => _ end) with (S (length next) <=? Z.to_nat rlen).
     rewrite Nat.leb_le. lia.
   Qed.
@@ -1858,7 +1858,7 @@ Section EquivLemmas.
     forall i j inp, length (substr inp i j) <= j-i.
   Proof.
     intros i j inp. unfold substr.
-    rewrite firstn_length. lia.
+    rewrite length_firstn. lia.
   Qed.
 
   Lemma indexing_nat_to_int {A}:
@@ -1961,12 +1961,12 @@ Section EquivLemmas.
     decide (Z.to_nat startIdx + n < length s).
     - (* firstn is actually truncating stuff *)
       rewrite <- nth_error_app1 with (l' := skipn n (skipn (Z.to_nat startIdx) s)).
-      2: { rewrite firstn_length_le; auto. rewrite skipn_length. lia. }
+      2: { rewrite firstn_length_le; auto. rewrite length_skipn. lia. }
       rewrite firstn_skipn.
       rewrite nth_error_skipn; auto.
     - (* firstn leaves the skipn unchanged *)
       rewrite firstn_all2.
-      2: { rewrite skipn_length. lia. }
+      2: { rewrite length_skipn. lia. }
       rewrite nth_error_skipn; auto.
   Qed.
 
@@ -1990,8 +1990,8 @@ Section EquivLemmas.
     - replace (length (skipn (length (rev pref)) str0)) with (length next).
       2: { rewrite <- Heqstr0. rewrite skipn_app, skipn_all, Nat.sub_diag. reflexivity. }
       apply List.Indexing.Int.success_bounds in Hindexing. rewrite <- Heqstr0 in Hindexing.
-      rewrite app_length, rev_length in Hindexing. lia.
-    - rewrite rev_length, Hlenpref. auto.
+      rewrite length_app, length_rev in Hindexing. lia.
+    - rewrite length_rev, Hlenpref. auto.
   Qed.
 
   Lemma nth_error_firstn {A}:
@@ -2031,10 +2031,10 @@ Section EquivLemmas.
     simpl in *.
     replace (rev _) with (firstn (Z.to_nat rlen) (skipn (end_ind - Z.to_nat rlen) str0)).
     2: { apply (f_equal (skipn (end_ind - Z.to_nat rlen))) in Heqstr0. rewrite <- Heqstr0.
-    rewrite skipn_app, rev_length. replace (end_ind - _ - length pref) with 0 by lia. simpl.
-    rewrite firstn_app, skipn_length, rev_length. replace (Z.to_nat rlen - _) with 0 by lia.
+    rewrite skipn_app, length_rev. replace (end_ind - _ - length pref) with 0 by lia. simpl.
+    rewrite firstn_app, length_skipn, length_rev. replace (Z.to_nat rlen - _) with 0 by lia.
     simpl. rewrite app_nil_r. rewrite skipn_rev. replace (length pref - _) with (Z.to_nat rlen) by lia.
-    rewrite firstn_all2. 2: { rewrite rev_length. apply firstn_le_length. } reflexivity. }
+    rewrite firstn_all2. 2: { rewrite length_rev. apply firstn_le_length. } reflexivity. }
     replace (end_ind - Z.to_nat rlen) with (Z.to_nat (Z.of_nat end_ind - rlen)) by lia.
     apply indexing_firstn_skipn; auto.
   Qed.
@@ -2107,13 +2107,13 @@ Section EquivLemmas.
         replace (nth_error (substr _ _ _) i) with (Some rsi) by (symmetry; eauto using backref_get_ref).
         rewrite neqb_eq in Hdiff. simpl. f_equal. congruence.
       + replace (nth_error _ i) with (None (A := Character)).
-        2: { symmetry. apply nth_error_None. rewrite map_length, firstn_length. lia. }
+        2: { symmetry. apply nth_error_None. rewrite length_map, length_firstn. lia. }
         replace (nth_error _ i) with (None (A := Character)).
         2: { symmetry. apply nth_error_None. transitivity (Z.to_nat endIdx - Z.to_nat startIdx). 2: lia.
-          rewrite map_length. apply substr_len. }
+          rewrite length_map. apply substr_len. }
         reflexivity.
   Qed.
-  
+
   (* Backward direction; mostly copy-pasting forward proof *)
   Lemma exists_diff_iff_bwd:
     forall ms next pref startIdx endIdx beginMatch rlen existsdiff,
@@ -2170,10 +2170,10 @@ Section EquivLemmas.
         replace (nth_error (substr _ _ _) i) with (Some rsi) by (symmetry; eauto using backref_get_ref).
         rewrite neqb_eq in Hdiff. simpl. f_equal. congruence.
       + replace (nth_error _ i) with (None (A := Character)).
-        2: { symmetry. apply nth_error_None. rewrite map_length, rev_length, firstn_length. lia. }
+        2: { symmetry. apply nth_error_None. rewrite length_map, length_rev, length_firstn. lia. }
         replace (nth_error _ i) with (None (A := Character)).
         2: { symmetry. apply nth_error_None. transitivity (Z.to_nat endIdx - Z.to_nat startIdx). 2: lia.
-          rewrite map_length. apply substr_len. }
+          rewrite length_map. apply substr_len. }
         reflexivity.
   Qed.
 
@@ -2195,8 +2195,8 @@ Section EquivLemmas.
     inversion Hmsinp as [str0' endIndOrig cap next' pref' Hlenpref Heqstr0 Heqms]. inversion Hinpcompat as [next'' pref'' str0'' Heqstr0bis Heqnext'' Heqpref''].
     subst next' next'' pref' pref'' ms str0''. simpl in *.
     split; constructor.
-    - rewrite app_length, rev_length, firstn_length_le; try lia.
-      apply (f_equal (length (A := Character))) in Heqstr0. rewrite app_length, rev_length in Heqstr0. lia.
+    - rewrite length_app, length_rev, firstn_length_le; try lia.
+      apply (f_equal (length (A := Character))) in Heqstr0. rewrite length_app, length_rev in Heqstr0. lia.
     - rewrite rev_app_distr. rewrite <- app_assoc. rewrite rev_involutive, firstn_skipn. auto.
     - rewrite rev_app_distr. rewrite <- app_assoc. rewrite rev_involutive, firstn_skipn. auto.
   Qed.
@@ -2219,7 +2219,7 @@ Section EquivLemmas.
     inversion Hmsinp as [str0' endIndOrig cap next' pref' Hlenpref Heqstr0 Heqms]. inversion Hinpcompat as [next'' pref'' str0'' Heqstr0bis Heqnext'' Heqpref''].
     subst next' next'' pref' pref'' ms str0''. simpl in *.
     split; constructor.
-    - rewrite skipn_length. lia.
+    - rewrite length_skipn. lia.
     - rewrite app_assoc. rewrite <- rev_app_distr. rewrite firstn_skipn. auto.
     - rewrite app_assoc. rewrite <- rev_app_distr. rewrite firstn_skipn. auto.
   Qed.
@@ -2233,7 +2233,7 @@ Section EquivLemmas.
   Proof.
     intros next pref inp' rlen startIdx endIdx -> Hrlennneg Hfirstn_next_substr ->.
     rewrite <- Hfirstn_next_substr.
-    simpl. rewrite app_length, rev_length. lia. 
+    simpl. rewrite length_app, length_rev. lia.
   Qed.
 
   Lemma backref_inp'_idx_bwd:
@@ -2245,7 +2245,7 @@ Section EquivLemmas.
   Proof.
     intros next pref inp' rlen startIdx endIdx -> Hrlennneg Hrlenle Hfirstn_pref_substr ->.
     rewrite <- Hfirstn_pref_substr.
-    simpl. rewrite rev_length, skipn_length, firstn_length_le; lia.
+    simpl. rewrite length_rev, length_skipn, firstn_length_le; lia.
   Qed.
 
 
diff --git a/WarblreEquiv/EquivMain.v b/WarblreEquiv/EquivMain.v
index 12607b4..5669d4b 100644
--- a/WarblreEquiv/EquivMain.v
+++ b/WarblreEquiv/EquivMain.v
@@ -4,7 +4,7 @@ From Linden Require Import Equiv EquivDef LWParameters RegexpTranslation
   Parameters ResultTranslation.
 From Warblre Require Import Patterns RegExpRecord Parameters Semantics
   Result Base Notation Match.
-From Coq Require Import List Lia PeanoNat ZArith DecidableClass.
+From Stdlib Require Import List Lia PeanoNat ZArith DecidableClass.
 Import Match.
 Import Notation.
 Import ListNotations.
@@ -26,7 +26,7 @@ Section EquivMain.
     Definition init_match_state (str0: string) (idx: nat) (rer: RegExpRecord): MatchState :=
       let cap := List.repeat undefined (RegExpRecord.capturingGroupsCount rer) in
       match_state str0 (Z.of_nat idx) cap.
-    
+
     (* Such an initial match state is equivalent to the empty group map... *)
     Lemma init_ms_equiv_empty:
       forall str0 idx rer, equiv_groupmap_ms GroupMap.empty (init_match_state str0 idx rer).
@@ -61,7 +61,7 @@ Section EquivMain.
     Qed.
 
   End InitState.
-  
+
 
   (** ** Plugging the identity MatcherContinuation into a Matcher compiled from some root regexp *)
   Theorem equiv_matcher_idmcont_compsucc:
@@ -93,7 +93,7 @@ Section EquivMain.
       (idx inp <=? length (input_str inp)) = true.
   Proof.
     intros [next pref]. apply Nat.leb_le.
-    simpl. rewrite app_length, rev_length. lia.
+    simpl. rewrite length_app, length_rev. lia.
   Qed.
 
   Lemma input_compat_self:
diff --git a/WarblreEquiv/GroupMapMS.v b/WarblreEquiv/GroupMapMS.v
index cf17dae..96cee41 100644
--- a/WarblreEquiv/GroupMapMS.v
+++ b/WarblreEquiv/GroupMapMS.v
@@ -1,4 +1,4 @@
-From Coq Require Import ZArith List.
+From Stdlib Require Import ZArith List.
 From Linden Require Import Chars Groups Tree LWParameters Parameters.
 From Warblre Require Import Notation Result Errors Parameters Base Patterns.
 Import Notation.
diff --git a/WarblreEquiv/LKFactorization.v b/WarblreEquiv/LKFactorization.v
index 6d01a88..9d7cfa7 100644
--- a/WarblreEquiv/LKFactorization.v
+++ b/WarblreEquiv/LKFactorization.v
@@ -3,7 +3,7 @@ From Linden Require Import LWParameters Parameters Regex RegexpTranslation.
 Import Notation.
 Import Result.Notations.
 Import Patterns.
-From Coq Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 
 Local Open Scope result_flow.
diff --git a/WarblreEquiv/LWParameters.v b/WarblreEquiv/LWParameters.v
index 55991e1..d5e8d34 100644
--- a/WarblreEquiv/LWParameters.v
+++ b/WarblreEquiv/LWParameters.v
@@ -1,6 +1,6 @@
 From Warblre Require Import Parameters Typeclasses RegExpRecord Patterns Result Errors.
 From Linden Require Import Parameters Utils.
-From Coq Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 Import Result.Notations.
 Import Utils.List.
diff --git a/WarblreEquiv/ListLemmas.v b/WarblreEquiv/ListLemmas.v
index 61b16d4..5c90b1c 100644
--- a/WarblreEquiv/ListLemmas.v
+++ b/WarblreEquiv/ListLemmas.v
@@ -1,5 +1,5 @@
 From Warblre Require Import List.
-From Coq Require Import List Lia ZArith.
+From Stdlib Require Import List Lia ZArith.
 Import ListNotations.
 
 (** * Lemmas on lists *)
@@ -29,7 +29,7 @@ Lemma skipn_ind_inv {A: Type}:
 Proof.
   intros i1 i2 l Hi1valid Hi2valid Hskipn.
   apply (f_equal (length (A := A))) in Hskipn.
-  do 2 rewrite skipn_length in Hskipn.
+  do 2 rewrite length_skipn in Hskipn.
   lia.
 Qed.
 
@@ -45,11 +45,11 @@ Proof.
   intros pref next str0 endInd1 Hconcat Hlenpref.
   apply (f_equal (skipn (Z.to_nat endInd1))) in Hconcat.
   rewrite skipn_app in Hconcat.
-  rewrite rev_length in Hconcat.
+  rewrite length_rev in Hconcat.
   replace (Z.to_nat endInd1 - length pref) with 0 in Hconcat by lia.
   simpl in Hconcat.
   replace (Z.to_nat endInd1) with (length pref) in Hconcat by lia.
-  rewrite <- rev_length in Hconcat at 1.
+  rewrite <- length_rev in Hconcat at 1.
   rewrite skipn_all in Hconcat.
   now replace (Z.to_nat endInd1) with (length pref) by lia.
 Qed.
diff --git a/WarblreEquiv/MSInput.v b/WarblreEquiv/MSInput.v
index fd483d3..dd5a89b 100644
--- a/WarblreEquiv/MSInput.v
+++ b/WarblreEquiv/MSInput.v
@@ -1,4 +1,4 @@
-From Coq Require Import List ZArith Lia.
+From Stdlib Require Import List ZArith Lia.
 From Warblre Require Import Notation Parameters Match Base Result Typeclasses.
 Import Notation.
 Import Match.
@@ -108,16 +108,16 @@ Section MSInput.
     assert (end_ind' = end_ind) by lia. rewrite H in H8. clear H.
     f_equal.
     - apply (f_equal (skipn end_ind)) in H4, H6. rewrite skipn_app in H4, H6.
-      subst end_ind. rewrite rev_length in H4, H6.
+      subst end_ind. rewrite length_rev in H4, H6.
       replace (length pref - length pref') with 0 in H6 by lia. rewrite Nat.sub_diag in H4.
-      rewrite <- H8 in H6 at 1. rewrite <- rev_length in H6 at 1. rewrite <- rev_length in H4 at 1.
+      rewrite <- H8 in H6 at 1. rewrite <- length_rev in H6 at 1. rewrite <- length_rev in H4 at 1.
       rewrite skipn_all in H4, H6. simpl in H4, H6. congruence.
     - apply (f_equal (firstn end_ind)) in H4, H6. rewrite firstn_app in H4, H6.
-      subst end_ind. rewrite rev_length in H4, H6.
+      subst end_ind. rewrite length_rev in H4, H6.
       rewrite H8 in H6. rewrite Nat.sub_diag in H4, H6. rewrite <- H8 in H6 at 1.
-      rewrite <- rev_length in H4 at 1, H6 at 1. rewrite firstn_all in H4, H6.
+      rewrite <- length_rev in H4 at 1, H6 at 1. rewrite firstn_all in H4, H6.
       simpl in H4, H6. rewrite app_nil_r in H4, H6.
-      apply (f_equal (rev (A := Character))) in H4, H6. rewrite rev_involutive in H4, H6. congruence. 
+      apply (f_equal (rev (A := Character))) in H4, H6. rewrite rev_involutive in H4, H6. congruence.
   Qed.
 
   Lemma strict_suffix_irreflexive_bool:
@@ -146,7 +146,7 @@ Section MSInput.
     intros ms [next pref] Hmsinp.
     inversion Hmsinp. subst next0 pref0. simpl.
     subst end_ind. split. 1: lia.
-    rewrite <- H3, app_length, rev_length. lia.
+    rewrite <- H3, length_app, length_rev. lia.
   Qed.
 
   (* Corollary with a compatible input string. *)
@@ -184,7 +184,7 @@ Section MSInput.
     2: exfalso; eapply error_succ_abs; eauto.
     injection Hgetchr as ->.
     (* Any way to automate this from now on? *)
-    pose proof f_equal (@length Character) Hstr0 as Hstr0len. rewrite app_length in Hstr0len. rewrite <- rev_length in Hlenpref. rewrite <- Hstr0 in Hgetchr'.
+    pose proof f_equal (@length Character) Hstr0 as Hstr0len. rewrite length_app in Hstr0len. rewrite <- length_rev in Hlenpref. rewrite <- Hstr0 in Hgetchr'.
     rewrite nth_error_app2 in Hgetchr' by lia.
     replace (end_ind - length _) with 0 in Hgetchr' by lia.
     destruct next as [|x next']. 1: discriminate.
@@ -203,10 +203,10 @@ Section MSInput.
     inversion Hmatches as [str0 end_ind cap next pref0 Hlenpref Hstr0 Heqms Heqnext].
     subst ms pref0 next. simpl in *.
     split.
-    - apply (f_equal (@length Character)) in Hstr0. rewrite app_length, rev_length, Hlenpref in Hstr0. simpl in Hstr0. lia.
+    - apply (f_equal (@length Character)) in Hstr0. rewrite length_app, length_rev, Hlenpref in Hstr0. simpl in Hstr0. lia.
     - rewrite List.List.Indexing.Int.of_nat.
       unfold List.List.Indexing.Nat.indexing. rewrite <- Hstr0.
-      rewrite nth_error_app2. 2: rewrite rev_length; lia. replace (end_ind - _) with 0 by (rewrite rev_length; lia).
+      rewrite nth_error_app2. 2: rewrite length_rev; lia. replace (end_ind - _) with 0 by (rewrite length_rev; lia).
       auto.
   Qed.
 
@@ -225,9 +225,9 @@ Section MSInput.
     exists pref'. exists next. f_equal. f_equal.
     subst end_ind. replace (Z.of_nat _ - 1)%Z with (Z.of_nat (length pref')) in Hgetchr by lia. rewrite List.List.Indexing.Int.of_nat in Hgetchr.
     rewrite <- Hstr0 in Hgetchr. unfold List.List.Indexing.Nat.indexing in Hgetchr.
-    rewrite nth_error_app1 in Hgetchr. 2: { rewrite app_length, rev_length. simpl. lia. }
-    rewrite nth_error_app2 in Hgetchr. 2: { rewrite rev_length. reflexivity. }
-    replace (length _ - length _) with 0 in Hgetchr. 2: { rewrite rev_length. lia. }
+    rewrite nth_error_app1 in Hgetchr. 2: { rewrite length_app, length_rev. simpl. lia. }
+    rewrite nth_error_app2 in Hgetchr. 2: { rewrite length_rev. reflexivity. }
+    replace (length _ - length _) with 0 in Hgetchr. 2: { rewrite length_rev. lia. }
 
     simpl in *. now injection Hgetchr.
   Qed.
@@ -243,8 +243,8 @@ Section MSInput.
     replace (Z.of_nat end_ind - 1)%Z with (Z.of_nat (length pref)) by lia.
     rewrite List.List.Indexing.Int.of_nat.
     unfold List.List.Indexing.Nat.indexing. rewrite <- Hstr0.
-    rewrite nth_error_app1. 2: { rewrite app_length, rev_length. simpl. lia. }
-    rewrite nth_error_app2. 2: { rewrite rev_length. reflexivity. }
-    rewrite rev_length, Nat.sub_diag. reflexivity.
+    rewrite nth_error_app1. 2: { rewrite length_app, length_rev. simpl. lia. }
+    rewrite nth_error_app2. 2: { rewrite length_rev. reflexivity. }
+    rewrite length_rev, Nat.sub_diag. reflexivity.
   Qed.
 End MSInput.
diff --git a/WarblreEquiv/NumericLemmas.v b/WarblreEquiv/NumericLemmas.v
index 9aed778..7a6c6f0 100644
--- a/WarblreEquiv/NumericLemmas.v
+++ b/WarblreEquiv/NumericLemmas.v
@@ -1,5 +1,5 @@
 From Warblre Require Import Numeric.
-From Coq Require Import Lia.
+From Stdlib Require Import Lia.
 
 (** * Lemmas about Warblre's `non_neg_integer_or_inf` (NoI) *)
 
diff --git a/WarblreEquiv/RegexpTranslation.v b/WarblreEquiv/RegexpTranslation.v
index 95ff442..bbee3d2 100644
--- a/WarblreEquiv/RegexpTranslation.v
+++ b/WarblreEquiv/RegexpTranslation.v
@@ -6,9 +6,9 @@ Import Notation.
 Import Result.
 Import Result.Notations.
 Local Open Scope result_flow.
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
-Require Import PeanoNat Lia.
+From Stdlib Require Import PeanoNat Lia.
 
 (** * Syntactic equivalence between Warblre regexes and Linden regexes
 and translation from Warblre to Linden regexes *)
@@ -44,7 +44,7 @@ Section RegexpTranslation.
 
   Definition buildnm (wr:Patterns.Regex) : namedmap :=
     fst (buildnm' wr [] 0).
-  
+
   (* Computes the number of capture groups of the regex r. *)
   Fixpoint num_groups (r: regex): nat := (* actually len (def_groups r); TODO replace later or prove lemma *)
     match r with
@@ -173,7 +173,7 @@ Section RegexpTranslation.
   | Equiv_backref: forall (n: nat) (gid: positive_integer) nm,
       equiv_regex' (Patterns.AtomEsc (Patterns.DecimalEsc gid)) (Backreference (positive_to_nat gid)) n nm
   | Equiv_named_backref: forall n nm name gid,
-      nameidx nm name = Some gid -> 
+      nameidx nm name = Some gid ->
       equiv_regex' (Patterns.AtomEsc (Patterns.GroupEsc name)) (Backreference gid) n nm
   | Equiv_atom_CharacterClassEscape:
     forall (esc: Patterns.CharacterClassEscape) (cd: char_descr) (n: nat) nm,
@@ -420,7 +420,7 @@ Section RegexpTranslation.
       remember ((map (fun '(fst, snd) => countLeftCapturingParensBefore fst snd)
             (groupSpecifiersThatMatch _ ctx name))) as l0 in *.
       apply in_len1_eq with (l := l0); auto.
-      rewrite Heql0, map_length. auto.
+      rewrite Heql0, length_map. auto.
     Qed.
   End Buildnm_GSMatch.
 
@@ -453,7 +453,7 @@ Section RegexpTranslation.
 
     Definition asciiEsc_singleCharacter_numValue (l: AsciiLetter): nat :=
       NonNegInt.modulo (AsciiLetter.numeric_value l) 32.
-    
+
     Definition characterEscape_singleCharacter_numValue (esc: Patterns.CharacterEscape): nat :=
       match esc with
       | Patterns.ControlEsc esc => controlEsc_singleCharacter_numValue esc
@@ -473,10 +473,10 @@ Section RegexpTranslation.
     Definition atomesc_to_linden (ae: Patterns.AtomEscape) (nm:namedmap): Result regex wl_transl_error :=
       match ae with
       | Patterns.DecimalEsc gid => Success (Backreference (positive_to_nat gid))
-      | Patterns.ACharacterClassEsc esc => 
+      | Patterns.ACharacterClassEsc esc =>
           let cd := characterClassEsc_to_linden esc in
           Success (Character cd)
-      | Patterns.ACharacterEsc esc => 
+      | Patterns.ACharacterEsc esc =>
           let cd := characterEscape_to_linden esc in
           Success (Character cd)
       | Patterns.GroupEsc gn =>
@@ -501,7 +501,7 @@ Section RegexpTranslation.
       | Patterns.CCharacterClassEsc esc => Error WlMalformed
       | Patterns.CCharacterEsc esc => Success (characterEscape_singleCharacter_numValue esc)
       end.
-    
+
     Definition classAtom_to_linden (ca: Patterns.ClassAtom): char_descr :=
       match ca with
       | Patterns.SourceCharacter c => CdSingle c
@@ -517,11 +517,11 @@ Section RegexpTranslation.
     Fixpoint classRanges_to_linden (cr: Patterns.ClassRanges): Result char_descr wl_transl_error :=
       match cr with
       | Patterns.EmptyCR => Success CdEmpty
-      | Patterns.ClassAtomCR ca t => 
+      | Patterns.ClassAtomCR ca t =>
           let cda := classAtom_to_linden ca in
           let! cdt =<< classRanges_to_linden t in
           Success (CdUnion cda cdt)
-      | Patterns.RangeCR l h t => 
+      | Patterns.RangeCR l h t =>
           let! cl =<< classAtom_singleCharacter_numValue l in
           let! ch =<< classAtom_singleCharacter_numValue h in
           let! cdt =<< classRanges_to_linden t in
@@ -530,11 +530,11 @@ Section RegexpTranslation.
           else
             Error WlMalformed
       end.
-    
+
     Definition charclass_to_linden (cc: Patterns.CharClass): Result char_descr wl_transl_error :=
       match cc with
       | Patterns.NoninvertedCC crs => classRanges_to_linden crs
-      | Patterns.InvertedCC crs => 
+      | Patterns.InvertedCC crs =>
           let! cd =<< classRanges_to_linden crs in
           Success (CdInv cd)
       end.
@@ -546,7 +546,7 @@ Section RegexpTranslation.
       | Patterns.Question => Success (fun greedy => Quantified greedy 0 (NoI.N 1))
       | Patterns.RepExact n => Success (fun greedy => Quantified greedy n (NoI.N 0))
       | Patterns.RepPartialRange n => Success (fun greedy => Quantified greedy n +∞)
-      | Patterns.RepRange mini maxi => 
+      | Patterns.RepRange mini maxi =>
           if mini <=? maxi then
             Success (fun greedy => Quantified greedy mini (NoI.N (maxi-mini)))
           else
@@ -563,7 +563,7 @@ Section RegexpTranslation.
       | Patterns.Char chr => Success (Character (CdSingle chr))
       | Patterns.Dot => Success (Character CdDot)
       | Patterns.AtomEsc ae => atomesc_to_linden ae nm
-      | Patterns.CharacterClass cc => 
+      | Patterns.CharacterClass cc =>
           let! cd =<< charclass_to_linden cc in
           Success (Character cd)
       | Patterns.Disjunction wr1 wr2 =>
@@ -1052,7 +1052,7 @@ Section RegexpTranslation.
         destruct IHwr as [lrsub IHwr]. simpl in *.
         rewrite Nat.add_0_r in IHwr. setoid_rewrite IHwr. eexists. reflexivity.
     Qed.
-    
+
     Theorem earlyErrors_pass_translation:
       forall wr: Patterns.Regex,
         earlyErrors wr nil = Success false ->
@@ -1114,4 +1114,4 @@ Section SanityCheck.
     destruct patname_eq_dec. 2: contradiction.
     eexists. reflexivity.
   Qed.
-End SanityCheck.
\ No newline at end of file
+End SanityCheck.
diff --git a/WarblreEquiv/ResultTranslation.v b/WarblreEquiv/ResultTranslation.v
index 5d4b660..45690f8 100644
--- a/WarblreEquiv/ResultTranslation.v
+++ b/WarblreEquiv/ResultTranslation.v
@@ -47,13 +47,13 @@ Section ResultTranslation.
     | None => 0
     | Some ms => List.length (MatchState.captures ms)
     end.
-  
+
   Lemma ms_num_groups_refl:
     forall ms_opt, ms_num_groups ms_opt (num_captures_opt ms_opt).
   Proof.
     intros [ms|]; simpl; constructor; auto.
   Qed.
-  
+
   Lemma to_MatchState_equal:
     forall res_opt ms_opt n,
       ms_num_groups ms_opt n ->
@@ -68,8 +68,8 @@ Section ResultTranslation.
     unfold GroupMapMS.equiv_groupmap_ms in H0. simpl in H0.
     clear EQUIV H NUM_GROUPS.
     apply List.nth_ext with (d := None) (d' := None).
-    1: { rewrite List.map_length, List.seq_length. reflexivity. }
-    rewrite List.map_length, List.seq_length. intros n IN_BOUNDS.
+    1: { rewrite List.length_map, List.length_seq. reflexivity. }
+    rewrite List.length_map, List.length_seq. intros n IN_BOUNDS.
     set (g := fun gid_prec =>
         if gid_prec <? length cap then
           to_capture_range (GroupMap.find (S gid_prec) gm)
diff --git a/WarblreEquiv/Utils.v b/WarblreEquiv/Utils.v
index ba2617b..b23714a 100644
--- a/WarblreEquiv/Utils.v
+++ b/WarblreEquiv/Utils.v
@@ -1,4 +1,4 @@
-From Coq Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
 From Warblre Require Import Typeclasses.
 
diff --git a/WarblreEquiv/WarblreLemmas.v b/WarblreEquiv/WarblreLemmas.v
index 5f46363..f870acf 100644
--- a/WarblreEquiv/WarblreLemmas.v
+++ b/WarblreEquiv/WarblreLemmas.v
@@ -1,7 +1,7 @@
 From Warblre Require Import Match Notation Parameters RegExpRecord List Result
   Semantics Result.
 From Linden Require Import Chars MSInput.
-From Coq Require Import ZArith Lia List.
+From Stdlib Require Import ZArith Lia List.
 Import Notation.
 Import Result.Notations.
 Import Match.MatchState.
@@ -20,7 +20,7 @@ Proof.
   apply H.
 Qed.
 
-Lemma range_seq: forall base l, List.List.Range.Nat.Length.range base l = Coq.Lists.List.seq base l.
+Lemma range_seq: forall base l, List.List.Range.Nat.Length.range base l = Stdlib.Lists.List.seq base l.
 Proof.
   intros base l.
   revert base.
diff --git a/_CoqProject b/_CoqProject
deleted file mode 100644
index a6296ab..0000000
--- a/_CoqProject
+++ /dev/null
@@ -1 +0,0 @@
--Q _build/default Linden
diff --git a/archive/LazyPrefix.archived b/archive/LazyPrefix.archived
index 64f44fd..6e0da0b 100644
--- a/archive/LazyPrefix.archived
+++ b/archive/LazyPrefix.archived
@@ -1,6 +1,6 @@
-Require Import List.
+From Stdlib Require Import List.
 Import ListNotations.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 From Linden Require Import Regex Chars Groups Tree Semantics.
 Require String.
diff --git a/archive/Termination.archived b/archive/Termination.archived
index 4d66643..4a0e88b 100644
--- a/archive/Termination.archived
+++ b/archive/Termination.archived
@@ -1,7 +1,7 @@
 (** * Termination of the PikeTree and PïkeVM algorithm *)
 (* Archived: now completely subsumed by the PikeVM complexity proof in Engine/Complexity.v *)
 
-Require Import List Lia.
+From Stdlib Require Import List Lia.
 Require Import Init.Wf.
 Import ListNotations.
 
@@ -133,7 +133,7 @@ Qed.
 (* Note that this does not mean that all executions of PikeTree terminate (it is non-deterministic) *)
 (* but that a terminating execution can be started from any state *)
 Theorem piketree_weak_termination:
-  forall pts, 
+  forall pts,
   exists res, trc_pike_tree pts (PTSS_final res).
 Proof.
   intros pts. eapply piketree_can_finish. eauto.
@@ -168,7 +168,7 @@ Qed.
 (* Decreasing lexicographic order on the PikeVM execution *)
 Theorem pikevm_decreases:
   forall code pts1 pvs1 pvs2 m1,
-    stutter_wf rer code -> 
+    stutter_wf rer code ->
     pike_inv rer code pts1 pvs1 m1 ->
     pike_vm_seen_step rer code pvs1 pvs2 ->
     exists pts2, exists m2,
diff --git a/dune b/dune
index 260563a..cd1e9d6 100644
--- a/dune
+++ b/dune
@@ -1,6 +1,7 @@
 (include_subdirs qualified)
 
-(coq.theory
+(rocq.theory
  (name Linden)
  (package linden)
- (theories Warblre Ltac2))
\ No newline at end of file
+ (generate_project_file)
+ (theories Warblre Ltac2 Stdlib))
diff --git a/dune-project b/dune-project
index 5e4b243..9195809 100644
--- a/dune-project
+++ b/dune-project
@@ -1,10 +1,10 @@
-(lang dune 3.14)
+(lang dune 3.21)
 
 (name linden)
 
 (generate_opam_files true)
 
-(using coq 0.8)
+(using rocq 0.11)
 
 (homepage "https://github.com/epfl-systemf/Linden")
 (authors "Aurèle Barrière" "Victor Deng" "Clément Pit-Claudel")
@@ -16,5 +16,5 @@
  (name linden)
  (synopsis "Formal Verification for JavaScript Regular Expressions")
  (depends
-  (coq (= 8.18.0))
+  (rocq-prover (= 9.0.0))
   (warblre (= 0.1.0))))
diff --git a/linden.opam b/linden.opam
index 12a46d5..4fbff18 100644
--- a/linden.opam
+++ b/linden.opam
@@ -7,8 +7,8 @@ license: "MIT"
 homepage: "https://github.com/epfl-systemf/Linden"
 bug-reports: "https://github.com/epfl-systemf/Linden/issues"
 depends: [
-  "dune" {>= "3.14"}
-  "coq" {= "8.18.0"}
+  "dune" {>= "3.21"}
+  "rocq-prover" {= "9.0.0"}
   "warblre" {= "0.1.0"}
   "odoc" {with-doc}
 ]
@@ -26,3 +26,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
+x-maintenance-intent: ["(latest)"]