diff --git a/theories/VLSM/Lib/FinExtras.v b/theories/VLSM/Lib/FinExtras.v
index 3bec5d19..519a1aad 100644
--- a/theories/VLSM/Lib/FinExtras.v
+++ b/theories/VLSM/Lib/FinExtras.v
@@ -11,13 +11,6 @@ Fixpoint up_to_n_listing
   | S n' => n' :: up_to_n_listing n'
   end.
 
-Lemma up_to_n_listing_length
-  (n : nat)
-  : length (up_to_n_listing n) = n.
-Proof.
-  induction n; simpl; congruence.
-Qed.
-
 Lemma up_to_n_full
   (n : nat)
   : forall i, i < n <-> i ∈ up_to_n_listing n.
diff --git a/theories/VLSM/Lib/FinFunExtras.v b/theories/VLSM/Lib/FinFunExtras.v
index 063584f5..dbe3d35d 100644
--- a/theories/VLSM/Lib/FinFunExtras.v
+++ b/theories/VLSM/Lib/FinFunExtras.v
@@ -68,13 +68,4 @@ Proof.
   by destruct a;simpl;congruence.
 Qed.
 
-Lemma right_finite
-  (sum_finite : Listing sum_listing)
-  : Listing (right_listing sum_finite).
-Proof.
-  revert sum_finite.
-  apply map_option_listing with (g:=inr); [| done].
-  by destruct a;simpl;congruence.
-Qed.
-
 End sum_listing.
diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v
index f512e64d..6c220e81 100644
--- a/theories/VLSM/Lib/ListExtras.v
+++ b/theories/VLSM/Lib/ListExtras.v
@@ -6,13 +6,6 @@ From VLSM Require Import Lib.Preamble.
 (** * Utility lemmas about lists *)
 
 (** A list is empty if it has no members *)
-Lemma empty_nil [X:Type] (l:list X) :
-  (forall v, ~In v l) -> l = [].
-Proof.
-  clear.
-  destruct l as [| a]; [done |].
-  simpl. intro H. elim (H a). by left.
-Qed.
 
 (** It is decidable whether a list is null or not *)
 Lemma null_dec {S} (l : list S) : Decision (l = []).
@@ -59,14 +52,6 @@ Proof.
   by induction tl as [| hd tl IHl].
 Qed.
 
-Lemma remove_hd_last {X} :
-  forall (hd1 hd2 d1 d2 : X) (tl : list X),
-    List.last (hd1 :: hd2 :: tl) d1 = List.last (hd2 :: tl) d2.
-Proof.
-  intros. induction tl; [done |].
-  cbn in *. by destruct tl.
-Qed.
-
 Lemma unroll_last {S} : forall (random a : S) (l : list S),
   List.last (a :: l) random = List.last l a.
 Proof.
@@ -108,24 +93,6 @@ Proof.
   by destruct l; [|inversion Herr; apply unroll_last].
 Qed.
 
-Lemma incl_empty : forall A (l : list A),
-  incl l nil -> l = nil.
-Proof.
-  intros A [] H; [done |].
-  by destruct (H a); left.
-Qed.
-
-Lemma incl_singleton {A} : forall (l : list A) (a : A),
-  incl l [a] ->
-  forall b, In b l -> b = a.
-Proof.
-  intros. induction l; inversion H0; subst.
-  - destruct (H b); [by left | done | inversion H1].
-  - apply IHl; [| done].
-    apply incl_tran with (a0 :: l); [| done].
-    apply incl_tl. apply incl_refl.
-Qed.
-
 Lemma Exists_first
   {A : Type}
   (l : list A)
@@ -203,37 +170,12 @@ Proof.
   by split; intros Hincl x Hx; apply in_correct; apply Hincl.
 Qed.
 
-Lemma map_incl {A B} (f : B -> A) : forall s s',
-  incl s s' ->
-  incl (map f s) (map f s').
-Proof.
-  intros s s' Hincl fx Hin.
-  apply in_map_iff .
-  apply in_map_iff in Hin as (x & Heq & Hin). eauto.
-Qed.
-
 Definition app_cons {A}
   (a : A)
   (l : list A)
   : [a] ++ l = a :: l
   := eq_refl.
 
-Lemma append_nodup_left {A}:
-  forall (l1 l2 : list A), List.NoDup (l1 ++ l2) -> List.NoDup l1.
-Proof.
-  induction l1; intros.
-  - constructor.
-  - inversion H. apply IHl1 in H3. constructor; [| done].
-    rewrite in_app_iff in H2. itauto.
-Qed.
-
-Lemma append_nodup_right {A}:
-  forall (l1 l2 : list A), List.NoDup (l1 ++ l2) -> List.NoDup l2.
-Proof.
-  induction l1; cbn; intros; [done |].
-  inversion H. auto.
-Qed.
-
 Lemma last_is_last {A} : forall (l : list A) (x dummy: A),
   List.last (l ++ [x]) dummy = x.
 Proof.
@@ -260,12 +202,6 @@ Fixpoint is_member {W} `{StrictlyComparable W} (w : W) (l : list W) : bool :=
               end
   end.
 
-Definition compareb {A} `{StrictlyComparable A} (a1 a2 : A) : bool :=
-  match compare a1 a2 with
-  | Eq => true
-  | _ => false
-  end.
-
 Lemma is_member_correct {W} `{StrictlyComparable W}
   : forall l (w : W), is_member w l = true <-> In w l.
 Proof.
@@ -278,23 +214,6 @@ Proof.
     + rewrite <- compare_eq. rewrite <- compare_asymmetric in Hcmp. itauto congruence.
 Qed.
 
-Lemma is_member_correct' {W} `{StrictlyComparable W}
-  : forall l (w : W), is_member w l = false <-> ~ In w l.
-Proof.
-  intros.
-  rewrite <- is_member_correct.
-  split; [congruence |].
-  apply not_true_is_false.
-Qed.
-
-Lemma In_app_comm {X} : forall l1 l2 (x : X), In x (l1 ++ l2) <-> In x (l2 ++ l1).
-Proof.
-  intros l1 l2 x; split; intro H_in;
-  apply in_or_app; apply in_app_or in H_in;
-    destruct H_in as [cat | dog];
-    itauto.
-Qed.
-
 Lemma nth_error_last
   {A : Type}
   (l : list A)
@@ -348,39 +267,6 @@ Fixpoint list_prefix
     | S n, a :: l => a :: list_prefix l n
     end.
 
-Lemma list_prefix_split
-  {A : Type}
-  (l left right: list A)
-  (left_len : nat)
-  (Hlen : left_len = length left)
-  (Hsplit : l = left ++ right) :
-  list_prefix l left_len = left.
-Proof.
-  generalize dependent l.
-  generalize dependent left.
-  generalize dependent right.
-  generalize dependent left_len.
-  induction left_len.
-  - intros.
-    symmetry in Hlen.
-    rewrite length_zero_iff_nil in Hlen.
-    rewrite Hlen.
-    unfold list_prefix.
-    by destruct l.
-  - intros.
-    destruct left; [done |].
-    assert (left_len = length left).
-    {
-      simpl in Hlen.
-      inversion Hlen.
-      itauto.
-    }
-    specialize (IHleft_len right left H (left ++ right) eq_refl).
-    rewrite Hsplit.
-    simpl.
-    by rewrite IHleft_len.
-Qed.
-
 Lemma list_prefix_map
   {A B : Type}
   (f : A -> B)
@@ -522,25 +408,6 @@ Proof.
   by apply dsig_eq.
 Qed.
 
-Lemma list_annotate_eq
-  {A : Type}
-  (P : A -> Prop)
-  {Pdec : forall a, Decision (P a)}
-  (l1 : list A)
-  (Hl1 : Forall P l1)
-  (l2 : list A)
-  (Hl2 : Forall P l2)
-  : list_annotate P l1 Hl1 = list_annotate P l2 Hl2 <-> l1 = l2.
-Proof.
-  split; [|intro; subst; apply list_annotate_pi].
-  revert Hl1 l2 Hl2.
-  induction l1; destruct l2; simpl; intros.
-  1-3: done.
-  inversion H.
-  apply IHl1 in H2.
-  by subst.
-Qed.
-
 Lemma list_annotate_unroll
   {A : Type}
   (P : A -> Prop)
@@ -551,40 +418,6 @@ Lemma list_annotate_unroll
   : list_annotate P (a :: l) Hs = dexist a (Forall_hd Hs) ::  list_annotate P l (Forall_tl Hs).
 Proof. done. Qed.
 
-Lemma list_annotate_app
-  {A : Type}
-  (P : A -> Prop)
-  {Pdec : forall a, Decision (P a)}
-  (l1 l2 : list A)
-  (Hs : Forall P (l1 ++ l2))
-  : list_annotate P (l1 ++ l2) Hs = list_annotate P l1 (proj1 (proj1 (@Forall_app _ P l1 l2) Hs)) ++ list_annotate P l2 (proj2 (proj1 (@Forall_app _ P l1 l2) Hs)).
-Proof.
-  induction l1; [apply list_annotate_pi|].
-  simpl. f_equal.
-  - by apply dsig_eq.
-  - rewrite IHl1. f_equal; apply list_annotate_pi.
-Qed.
-
-Lemma nth_error_list_annotate
-  {A : Type}
-  (P : A -> Prop)
-  (Pdec : forall a, Decision (P a))
-  (l : list A)
-  (Hs : Forall P l)
-  (n : nat)
-  : exists (oa : option (dsig P)),
-    nth_error (list_annotate P l Hs) n = oa
-    /\ option_map (@proj1_sig _ _) oa = nth_error l n.
-Proof.
-  generalize dependent l.
-  induction n; intros [| a l] Hs.
-  - by exists None.
-  - inversion Hs; subst. exists (Some (dexist a (Forall_hd Hs))).
-    by rewrite list_annotate_unroll.
-  - by exists None.
-  - rewrite list_annotate_unroll; eauto.
-Qed.
-
 Fixpoint nth_error_filter_index
   {A} P `{∀ (x:A), Decision (P x)}
   (l : list A)
@@ -602,52 +435,6 @@ Fixpoint nth_error_filter_index
       option_map S (nth_error_filter_index P l n)
   end.
 
-Lemma nth_error_filter_index_le
-  {A} P `{∀ (x:A), Decision (P x)}
-  (l : list A)
-  (n1 n2 : nat)
-  (Hle : n1 <= n2)
-  (in1 in2 : nat)
-  (Hin1 : nth_error_filter_index P l n1 = Some in1)
-  (Hin2 : nth_error_filter_index P l n2 = Some in2)
-  : in1 <= in2.
-Proof.
-  generalize dependent in2.
-  generalize dependent in1.
-  generalize dependent n2.
-  generalize dependent n1.
-  induction l; intros.
-  - inversion Hin1.
-  - simpl in Hin1. simpl in Hin2.
-    destruct (decide (P a)).
-    + destruct n1; destruct n2.
-      * by inversion Hin1; inversion Hin2; subst.
-      * destruct (nth_error_filter_index P l n2)
-        ; inversion Hin1; inversion Hin2; subst.
-        lia.
-      * inversion Hle.
-      * { destruct in1, in2.
-        - lia.
-        - lia.
-        - destruct (nth_error_filter_index P l n2); inversion Hin2.
-        - assert (Hle' : n1 <= n2) by lia.
-          specialize (IHl n1 n2 Hle').
-          destruct (nth_error_filter_index P l n1) eqn:Hin1'; inversion Hin1;
-          subst; clear Hin1.
-          destruct (nth_error_filter_index P l n2) eqn:Hin2'; inversion Hin2
-          ; subst; clear Hin2.
-          specialize (IHl in1 eq_refl in2 eq_refl).
-          lia.
-        }
-    + specialize (IHl n1 n2 Hle).
-      destruct (nth_error_filter_index P l n1) eqn:Hin1'; inversion Hin1
-      ; subst; clear Hin1.
-      destruct (nth_error_filter_index P l n2) eqn:Hin2'; inversion Hin2
-      ; subst; clear Hin2.
-      specialize (IHl n0 eq_refl n3 eq_refl).
-      lia.
-Qed.
-
 Fixpoint Forall_filter
   {A : Type}
   (P : A -> Prop)
@@ -812,93 +599,6 @@ Proof.
   - by rewrite unroll_last, unroll_last.
 Qed.
 
-Lemma list_suffix_last_default
-  {A : Type}
-  (l : list A)
-  (i : nat)
-  (Hlast : i = length l)
-  (_default : A)
-  : List.last (list_suffix l i) _default  = _default.
-Proof.
-  revert l Hlast. induction i; intros [|a l] Hlast; try done.
-  apply IHi. by inversion Hlast.
-Qed.
-
-Lemma list_segment_nth
-  {A : Type}
-  (l : list A)
-  (n1 n2 : nat)
-  (Hn : n1 <= n2)
-  (i : nat)
-  (Hi1 : n1 <= i)
-  (Hi2 : i < n2)
-  : nth_error (list_segment l n1 n2) (i - n1) = nth_error l i.
-Proof.
-  unfold list_segment.
-  rewrite list_suffix_nth; [| done].
-  by apply list_prefix_nth.
-Qed.
-
-Lemma list_segment_app
-  {A : Type}
-  (l : list A)
-  (n1 n2 n3 : nat)
-  (H12 : n1 <= n2)
-  (H23 : n2 <= n3)
-  : list_segment l n1 n2 ++ list_segment l n2 n3 = list_segment l n1 n3.
-Proof.
-  assert (Hle : n1 <= n3) by lia.
-  specialize (list_prefix_segment_suffix l n1 n3 Hle); intro Hl1.
-  specialize (list_prefix_segment_suffix l n2 n3 H23); intro Hl2.
-  rewrite <- Hl2 in Hl1 at 4. clear Hl2.
-  repeat rewrite app_assoc in Hl1.
-  apply app_inv_tail in Hl1.
-  specialize (list_prefix_suffix (list_prefix l n2) n1); intro Hl2.
-  specialize (list_prefix_prefix l n1 n2 H12); intro Hl3.
-  rewrite Hl3 in Hl2.
-  rewrite <- Hl2 in Hl1.
-  rewrite <- app_assoc in Hl1.
-  by apply app_inv_head in Hl1.
-Qed.
-
-Lemma list_segment_singleton
-  {A : Type}
-  (l : list A)
-  (n : nat)
-  (a : A)
-  (Hnth : nth_error l n = Some a)
-  : list_segment l n (S n) = [a].
-Proof.
-  unfold list_segment.
-  assert (Hle : S n <= length l)
-    by (apply nth_error_length in Hnth; done).
-  assert (Hlt : n < length (list_prefix l (S n)))
-    by (rewrite list_prefix_length; try constructor; done).
-  specialize (list_suffix_last (list_prefix l (S n)) n Hlt a); intro Hlast1.
-  specialize (list_prefix_nth_last l n a Hnth a); intro Hlast2.
-  rewrite <- Hlast2 in Hlast1.
-  specialize (list_suffix_length (list_prefix l (S n)) n).
-  rewrite list_prefix_length; [| done].
-  intro Hlength.
-  assert (Hs: S n - n = 1) by lia.
-  rewrite Hs in Hlength.
-  remember (list_suffix (list_prefix l (S n)) n) as x.
-  clear -Hlength Hlast1.
-  destruct x; inversion Hlength.
-  destruct x; inversion H0.
-  by simpl in Hlast1; subst.
-Qed.
-
-Lemma nth_error_map
-  {A B : Type}
-  (f : A -> B)
-  (l : list A)
-  (n : nat)
-  : nth_error (List.map f l) n = option_map f (nth_error l n).
-Proof.
-  revert n. induction l; intros [| n]; firstorder.
-Qed.
-
 Lemma exists_finite
   `{finite.Finite index}
   (P : index -> Prop)
@@ -1016,15 +716,6 @@ Definition cat_option {A : Type} : list (option A) -> list A :=
 Example cat_option1 : cat_option [Some 1; Some 5; None; Some 6; None] = [1; 5; 6].
 Proof. itauto. Qed.
 
-Lemma cat_option_length
-  {A : Type}
-  (l : list (option A))
-    (Hfl : Forall (fun a => a <> None) l)
-  : length (cat_option l) = length l.
-Proof.
-  apply map_option_length; itauto.
-Qed.
-
 Lemma cat_option_length_le
   {A : Type}
   (l : list (option A))
@@ -1036,33 +727,6 @@ Proof.
     destruct (id a) eqn : eq_id; simpl in *; subst a; simpl; lia.
 Qed.
 
-Lemma cat_option_app
-  {A : Type}
-  (l1 l2 : list (option A)) :
-  cat_option (l1 ++ l2) = cat_option l1 ++ cat_option l2.
-Proof.
-  induction l1.
-  - simpl in *. itauto.
-  - by destruct a; cbn in *; rewrite IHl1.
-Qed.
-
-Lemma cat_option_nth
-  {A : Type}
-  (l : list (option A))
-  (Hfl : Forall (fun a => a <> None) l)
-  (n := length l)
-  (i : nat)
-  (Hi : i < n)
-  (dummya : A)
-  : Some (nth i (cat_option l) dummya) = (nth i l (Some dummya)).
-Proof.
-  specialize (@map_option_nth (option A) A id l). simpl in *.
-  intros.
-  unfold id in *.
-  apply H.
-  all : itauto.
-Qed.
-
 Lemma nth_error_eq
   {A : Type}
   (l1 l2 : list A)
@@ -1082,41 +746,6 @@ Proof.
 Qed.
 
 (* TODO remove (we have Exists_first) *)
-Lemma exists_first
-  {A : Type}
-  (l : list A)
-  (P : A -> Prop)
-  (Pdec : forall a : A, {P a } + {~P a})
-  (Hsomething : Exists P l) :
-  exists (prefix : list A)
-         (suffix : list A)
-         (first : A),
-         (P first) /\
-         l = prefix ++ [first] ++ suffix /\
-         ~Exists P prefix.
-Proof.
-  induction l.
-  - inversion Hsomething.
-  - destruct (Pdec a).
-    + exists [], l, a. rewrite Exists_nil. itauto.
-    + assert (Hl : Exists P l) by (inversion Hsomething; subst; done).
-      specialize (IHl Hl).
-      destruct IHl as [prefix [suffix [first [Hfirst [Heq Hprefix]]]]].
-      exists (a :: prefix), suffix, first. split_and!; subst; [done | done |].
-      by inversion 1; subst.
-Qed.
-
-Lemma in_fast
-  {A : Type}
-  (l : list A)
-  (a : A)
-  (b : A)
-  (Hin : In a (b :: l))
-  (Hneq : b <> a) :
-  In a l.
-Proof.
-  by destruct Hin.
-Qed.
 
 Fixpoint one_element_decompositions
   {A : Type}
@@ -1186,52 +815,6 @@ Definition two_element_decompositions
     )
     (one_element_decompositions l).
 
-Lemma in_two_element_decompositions_iff
-  {A : Type}
-  (l : list A)
-  (pre mid suf : list A)
-  (x y : A)
-  : In (pre, x, mid, y, suf) (two_element_decompositions l)
-  <-> pre ++ [x] ++ mid ++ [y] ++ suf = l.
-Proof.
-  unfold two_element_decompositions.
-  rewrite in_flat_map.
-  split.
-  - intros [((pre', x'), sufx) [Hdecx Hin]].
-    apply in_map_iff in Hin.
-    destruct Hin as [((mid', y'), suf') [Hdec Hin]].
-    inversion Hdec. subst. clear Hdec.
-    apply in_one_element_decompositions_iff in Hdecx.
-    apply in_one_element_decompositions_iff in Hin.
-    by subst.
-  - remember (mid ++ [y] ++ suf) as sufx.
-    intro H.
-    exists (pre, x, sufx). apply in_one_element_decompositions_iff in H.
-    split; [done |].
-    apply in_map_iff. exists (mid, y, suf).
-    by rewrite in_one_element_decompositions_iff.
-Qed.
-
-Lemma order_decompositions
-  {A : Type}
-  (pre1 suf1 pre2 suf2 : list A)
-  (Heq : pre1 ++ suf1 = pre2 ++ suf2)
-  : pre1 = pre2
-  \/ (exists suf1', pre1 = pre2 ++ suf1')
-  \/ (exists suf2', pre2 = pre1 ++ suf2').
-Proof.
-  remember (pre1 ++ suf1) as l.
-  revert pre1 suf1 pre2 suf2 Heql Heq.
-  induction l; intros.
-  - left. symmetry in Heql, Heq.
-    by apply app_nil in Heql as [-> ->], Heq as [-> ->].
-  - destruct pre1 as [| a1 pre1]; destruct pre2 as [|a2 pre2]. 1-3: eauto.
-    inversion Heql; subst a1; clear Heql.
-    inversion Heq; subst a2; clear Heq.
-    destruct (IHl pre1 suf1 pre2 suf2 H1 H2)
-          as [Heq | [[suf1' Hgt] | [suf2' Hlt]]]; subst; eauto.
-Qed.
-
 Lemma list_max_exists
    (l : list nat)
    (nz : list_max l > 0) :
@@ -1247,23 +830,6 @@ Proof.
       by rewrite H; left.
 Qed.
 
-Lemma list_max_exists2
-   (l : list nat)
-   (Hne : l <> []) :
-   In (list_max l) l.
-Proof.
-  destruct (list_max l) eqn : eq_max.
-  - destruct l;[itauto congruence|].
-    specialize (list_max_le (n :: l) 0) as Hle.
-    destruct Hle as [Hle _].
-    rewrite eq_max in Hle. spec Hle. apply Nat.le_refl.
-    rewrite Forall_forall in Hle.
-    specialize (Hle n). spec Hle; [left |].
-    simpl. lia.
-  - specialize (list_max_exists l) as Hmax.
-    spec Hmax. lia. rewrite <- eq_max. itauto.
-Qed.
-
 (* Returns all values which occur with maximum frequency in the given list.
    Note that these values are returned with their original multiplicity. *)
 
@@ -1416,13 +982,6 @@ Definition list_sum_project_right
   :=
   map_option sum_project_right x.
 
-Lemma fold_right_andb_false l:
-  fold_right andb false l = false.
-Proof.
-  induction l; [done |].
-  simpl. rewrite IHl. apply andb_false_r.
-Qed.
-
 Definition Listing_finite_transparent `{EqDecision A} {l : list A} (finite_l : Listing l) : finite.Finite A.
 Proof.
   exists l.
@@ -1515,62 +1074,17 @@ Inductive ForAllSuffix : list A -> Prop :=
   | SNil : P [] -> ForAllSuffix []
   | SHereAndFurther : forall a l, P (a :: l) -> ForAllSuffix l -> ForAllSuffix (a :: l).
 
-Lemma fsHere : forall l, ForAllSuffix l -> P l.
-Proof. by inversion 1. Qed.
-
 Lemma fsFurther : forall a l, ForAllSuffix (a :: l) -> ForAllSuffix l.
 Proof. by inversion 1. Qed.
 
-Lemma ForAll_list_suffix : forall m x, ForAllSuffix x -> ForAllSuffix (list_suffix x m).
-Proof.
-  induction m; simpl; intros [] **. 1-3: done.
-  by apply fsFurther in H; apply IHm.
-Qed.
-
-Lemma ForAllSuffix_induction
-  (Inv : list A -> Prop)
-  (InvThenP : forall l, Inv l -> P l)
-  (InvIsStable : forall a l, Inv (a :: l) -> Inv l)
-  : forall l, Inv l -> ForAllSuffix l.
-Proof.
-  induction l; intros.
-  - by constructor; apply InvThenP.
-  - constructor.
-    + by apply InvThenP.
-    + by eapply IHl, InvIsStable.
-Qed.
-
 End suffix_quantifiers.
 
-Lemma ForAllSuffix_subsumption [A : Type] (P Q : list A -> Prop)
-  (HPQ : forall l, P l -> Q l)
-  : forall l, ForAllSuffix P l -> ForAllSuffix Q l.
-Proof.
-  induction 1; constructor; auto.
-Qed.
-
 Definition ForAllSuffix1 [A : Type] (P : A -> Prop) : list A -> Prop :=
   ForAllSuffix (fun l => match l with | [] => True | a :: _ => P a end).
 
-Lemma ForAllSuffix1_Forall [A : Type] (P : A -> Prop)
-  : forall l, ForAllSuffix1 P l <-> Forall P l.
-Proof.
-  split; induction 1; constructor; auto.
-Qed.
-
 Definition ExistsSuffix1 [A : Type] (P : A -> Prop) : list A -> Prop :=
   ExistsSuffix (fun l => match l with | [] => False | a :: _ => P a end).
 
-Lemma ExistsSuffix1_Exists [A : Type] (P : A -> Prop)
-  : forall l, ExistsSuffix1 P l <-> Exists P l.
-Proof.
-  split; induction 1.
-  - by destruct l; [| left].
-  - by right.
-  - by left.
-  - by right.
-Qed.
-
 Definition ForAllSuffix2 [A : Type] (R : A -> A -> Prop) : list A -> Prop :=
   ForAllSuffix (fun l => match l with | a :: b :: _ => R a b | _ => True end).
 
@@ -1601,14 +1115,6 @@ Proof.
   - apply IHl. by eapply fsFurther2_transitive.
 Qed.
 
-
-Lemma list_subseteq_tran : forall (A : Type) (l m n : list A),
- l ⊆ m → m ⊆ n → l ⊆ n.
-Proof.
-  intros A l m n Hlm Hmn x y.
-  by apply Hmn, Hlm.
-Qed.
-
 #[global] Instance list_subseteq_dec `{EqDecision A} : RelDecision (@subseteq (list A) _).
 Proof.
   intros x.
@@ -1696,12 +1202,6 @@ Proof.
 Qed.
 
 (** If <<n>> is zero, then the result of [lastn] is [[]]. *)
-Lemma lastn_0 :
-  forall {A : Type} (l : list A),
-    lastn 0 l = [].
-Proof.
-  by intros A l; unfold lastn; rewrite take_0.
-Qed.
 
 (** If <<n>> is greater than the length of the list, [lastn] returns the whole list. *)
 Lemma lastn_ge :
@@ -1749,34 +1249,8 @@ Qed.
 
 (** If <<n1>> is less than (or equal to) <<n2>>, then <<lastn n1 l>> is shorter than
     <<lastn n2 l>> and therefore is its suffix. *)
-Lemma suffix_lastn :
-  forall {A : Type} (l : list A) (n1 n2 : nat),
-    n1 <= n2 -> suffix (lastn n1 l) (lastn n2 l).
-Proof.
-  intros A l n1 n2 Hle.
-  unfold lastn.
-  apply suffix_rev.
-  exists (take (n2 - n1) (drop n1 (rev l))).
-  rewrite take_take_drop.
-  by f_equal; lia.
-Qed.
 
 (** The length of <<lastn n l>> is the smaller of <<n>> and the length of <<l>>. *)
-Lemma length_lastn :
-  forall {A : Type} (n : nat) (l : list A),
-    length (lastn n l) = min n (length l).
-Proof.
-  intros A n l.
-  unfold lastn.
-  by rewrite rev_length, take_length, rev_length.
-Qed.
-
-Program Definition not_null_element
-  `{EqDecision A} [l : list A] (Hl : l <> []) : dsig (fun i => i ∈ l) :=
-    dexist (is_Some_proj (proj2 (head_is_Some l) Hl)) _.
-Next Obligation.
-  by intros A ? [| h t] ?; [| left].
-Qed.
 
 Program Definition element_of_subseteq
   `{EqDecision A} [l1 l2 : list A] (Hsub : l1 ⊆ l2)
@@ -1785,8 +1259,3 @@ Program Definition element_of_subseteq
 Next Obligation.
   by intros; cbn; destruct_dec_sig di i Hi Heq; subst; apply Hsub.
 Qed.
-
-Definition element_of_filter
-  `{EqDecision A} [P : A -> Prop] `{∀ x, Decision (P x)} [l : list A]
-  : dsig (fun i => i ∈ filter P l) -> dsig (fun i => i ∈ l) :=
-  element_of_subseteq (list_filter_subseteq P l).
diff --git a/theories/VLSM/Lib/ListSetExtras.v b/theories/VLSM/Lib/ListSetExtras.v
index 9de3f9e6..fc72bd5d 100644
--- a/theories/VLSM/Lib/ListSetExtras.v
+++ b/theories/VLSM/Lib/ListSetExtras.v
@@ -169,34 +169,6 @@ Proof.
     + right. apply IHss. by exists x.
 Qed.
 
-Lemma set_union_iterated_subseteq
-  `{EqDecision A}
-  (ss ss': list (set A))
-  (Hincl : ss ⊆ ss') :
-  (fold_right set_union [] ss) ⊆
-  (fold_right set_union [] ss').
-Proof.
-  intros a H.
-  apply set_union_in_iterated in H.
-  apply set_union_in_iterated.
-  rewrite Exists_exists in *.
-  destruct H as [x [Hx Ha]].
-  exists x.
-  unfold incl in Hincl.
-  split; [| done].
-  by apply Hincl.
-Qed.
-
-Lemma set_union_empty_left `{EqDecision A}  : forall (s : list A),
-  NoDup s -> set_eq (set_union [] s) s.
-Proof.
-  intros. split; intros x Hin.
-  - apply set_union_elim in Hin. destruct Hin.
-    + inversion H0.
-    + done.
-  - by apply set_union_intro; right.
-Qed.
-
 Lemma map_list_subseteq {A B} : forall (f : B -> A) (s s' : list B),
   s ⊆ s' -> (map f s) ⊆ (map f s').
 Proof.
@@ -278,25 +250,6 @@ Proof.
   by split; destruct H; apply set_map_subseteq.
 Qed.
 
-Lemma set_map_singleton {A B} `{EqDecision A} (f : B -> A) : forall s a,
-  set_map f s = [a] ->
-  forall b, b ∈ s -> f b = a.
-Proof.
-  intros. apply (set_map_elem_of f) in H0. rewrite H in H0. apply elem_of_cons in H0.
-  destruct H0; [done | inversion H0].
-Qed.
-
-Lemma filter_set_add `{StrictlyComparable X} P
-  `{∀ (x:X), Decision (P x)} :
-  forall (l:list X) x, ~ P x ->
-  filter P l = filter P (set_add x l).
-Proof.
-  induction l as [|hd tl IHl]; intros x H_false; cbn.
-  - by rewrite decide_False.
-  - destruct (decide (x = hd)); cbn; [done |].
-    by destruct (decide (P hd)); rewrite <- (IHl).
-Qed.
-
 Lemma set_add_ignore `{StrictlyComparable X} :
   forall (l : list X) (x : X),
     x ∈ l ->
@@ -338,26 +291,6 @@ Proof.
   by intros x y s ->; cbn; rewrite decide_True.
 Qed.
 
-Lemma set_remove_nodup_1 `{EqDecision A} : forall x (s : list A),
-  NoDup (set_remove x s) ->
-  ~ x ∈ (set_remove x s) ->
-  NoDup s.
-Proof.
-  induction s; intros.
-  - constructor.
-  - simpl in H0 . destruct (decide (x = a)).
-    + cbn in H; subst. constructor; [done |]. by rewrite decide_True in H.
-    + rewrite elem_of_cons in H0.
-      simpl in H.
-      rewrite decide_False in H; auto.
-      inversion H; subst.
-      constructor.
-      * intro Ha; apply (set_remove_3 _ x) in Ha; auto.
-      * apply IHs; [done |].
-        intro Hx.
-        by contradict H0; right.
-Qed.
-
 Lemma set_remove_elem_of_iff `{EqDecision A} :  forall x y (s : list A),
   NoDup s ->
   y ∈ s ->
@@ -409,18 +342,6 @@ Proof.
   split; intros a Hin; rewrite set_remove_iff in *; itauto.
 Qed.
 
-Lemma subseteq_remove_union `{EqDecision A} : forall x (s1 s2 : list A),
-  NoDup s1 ->
-  NoDup s2 ->
-  (set_remove x (set_union s1 s2)) ⊆
-  (set_union s1 (set_remove x s2)).
-Proof.
-  intros. intros y Hin. apply set_remove_iff in Hin.
-  - apply set_union_intro. destruct Hin. apply set_union_elim in H1.
-    rewrite set_remove_iff; itauto.
-  - by apply set_union_nodup.
-Qed.
-
 Lemma set_eq_remove_union_elem_of  `{EqDecision A} : forall x (s1 s2 : list A),
   NoDup s1 ->
   NoDup s2 ->
@@ -463,15 +384,6 @@ Qed.
 for the second argument.
 *)
 (* TODO(palmskog): consider submitting a PR to Coq's stdlib. *)
-Lemma set_diff_nodup' `{EqDecision A} (l l' : list A)
-  : NoDup l -> NoDup (set_diff l l').
-Proof.
-induction 1 as [|x l H H' IH]; simpl.
-- constructor.
-- case_decide.
-  + by apply IH.
-  + by apply set_add_nodup, IH.
-Qed.
 
 Lemma diff_app_nodup `{EqDecision A} : forall (s1 s2 : list A),
   NoDup s1 ->
@@ -497,16 +409,6 @@ Proof.
     rewrite Heq, IHlv; itauto.
 Qed.
 
-Lemma set_union_iterated_empty `{EqDecision A} :
-  forall ss : list (set A),
-    (forall s : list A, s ∈ ss -> s = []) -> fold_right set_union [] ss = [].
-Proof.
-  induction ss; [done |]; cbn; intros H.
-  rewrite IHss; cycle 1.
-  - by intros s Hel; apply H; right.
-  - by cbn; apply H; left.
-Qed.
-
 (** For each element X of l1, exactly one occurrence of X is removed
    from l2. If no such occurrence exists, nothing happens. *)
 
@@ -533,26 +435,6 @@ Proof.
     by apply set_remove_1, IHl1 in Hin.
 Qed.
 
-Lemma set_prod_nodup `(s1: set A) `(s2: set B):
-  NoDup s1 ->
-  NoDup s2 ->
-  NoDup (set_prod s1 s2).
-Proof.
-  intros Hs1 HS2.
-  induction Hs1.
-  + constructor.
-  + simpl.
-    apply nodup_append.
-    * apply NoDup_fmap; [congruence | done].
-    * done.
-    * intros [a b].
-      rewrite elem_of_list_fmap, elem_of_list_prod.
-      intros [_ [[= <- _] _]]. itauto.
-    * intros [a b].
-      rewrite elem_of_list_prod, elem_of_list_fmap.
-      intros [Ha _] [_ [[= Hax _] _]]. congruence.
-Qed.
-
 (** An alternative to [set_diff].
     Unlike [set_diff], the result may contain
     duplicates if the first argument list <<l>> does.
@@ -569,27 +451,6 @@ Definition set_diff_filter `{EqDecision A} (l r : list A) :=
    The characteristic membership property, parallel to
    [set_diff_iff].
  *)
-Lemma set_diff_filter_iff `{EqDecision A} (a:A) l r:
-  a ∈ (set_diff_filter l r) <-> (a ∈ l /\ ~a ∈ r).
-Proof.
-  induction l;simpl.
-  - cbn. split; intros; [|itauto].
-    inversion H.
-  - unfold set_diff_filter in *.
-    rewrite filter_cons.
-    destruct (decide (~ a0 ∈ r)).
-    * rewrite 2 elem_of_cons, IHl.
-      split; itauto congruence.
-    * rewrite elem_of_cons.
-      split;itauto congruence.
-Qed.
-
-Lemma set_diff_filter_nodup `{EqDecision A} (l r:list A):
-  NoDup l -> NoDup (set_diff_filter l r).
-Proof.
-  intros H.
-  by apply NoDup_filter.
-Qed.
 
 (**
    Prove that subtracting a superset cannot produce
@@ -682,20 +543,6 @@ Add Parametric Morphism A : (@elem_of_list A)
   with signature @eq A ==> @list_subseteq A ==> Basics.impl as set_elem_of_subseteq.
 Proof. firstorder. Qed.
 
-Lemma set_union_iterated_preserves_prop
-  `{EqDecision A}
-  (ss : list (set A))
-  (P : A -> Prop)
-  (Hp : forall (s : set A), forall (a : A), (s ∈ ss /\ a ∈ s) -> P a) :
-  forall (a : A), a ∈ (fold_right set_union [] ss) -> P a.
-Proof.
-  intros.
-  apply set_union_in_iterated in H. rewrite Exists_exists in H.
-  destruct H as [s [Hins Hina]].
-  apply Hp with (s := s).
-  itauto.
-Qed.
-
 Lemma filter_set_eq {X} P Q
  `{∀ (x:X), Decision (P x)} `{∀ (x:X), Decision (Q x)}
    (l : list X)
diff --git a/theories/VLSM/Lib/RealsExtras.v b/theories/VLSM/Lib/RealsExtras.v
index 75ef3b0e..a966fedb 100644
--- a/theories/VLSM/Lib/RealsExtras.v
+++ b/theories/VLSM/Lib/RealsExtras.v
@@ -3,22 +3,6 @@ From stdpp Require Import prelude.
 
 (** * Real number utility lemmas *)
 
-(** This lemma is needed in fault_weight_state_backwards **)
-Lemma Rplusminus_assoc : forall r1 r2 r3,
-  (r1 + r2 - r3)%R = (r1 + (r2 - r3))%R.
-Proof.
-  intros. unfold Rminus.
-  apply Rplus_assoc.
-Qed.
-
-(** This lemma is needed in fault_weight_state_sorted_subset **)
-Lemma Rplusminus_assoc_r : forall r1 r2 r3,
-  (r1 - r2 + r3)%R = (r1 + (- r2 + r3))%R.
-Proof.
-  intros. unfold Rminus.
-  apply Rplus_assoc.
-Qed.
-
 (** This lemma is needed in fault_weight_state_sorted_subset **)
 Lemma Rplus_opp_l : forall r, (Ropp r + r)%R = 0%R.
 Proof.
@@ -27,36 +11,6 @@ Proof.
   apply Rplus_opp_r.
 Qed.
 
-(** This lemma is needed in fault_weight_state_sorted_subset **)
-Lemma Rplus_ge_reg_neg_r : forall r1 r2 r3,
-  (r2 <= 0)%R -> (r3 <= r1 + r2)%R -> (r3 <= r1)%R.
-Proof.
-  intros.
-  apply Rge_le.
-  apply Rle_ge in H.
-  apply Rle_ge in H0.
-  apply (Rplus_ge_reg_neg_r r1 r2 r3 H H0).
-Qed.
-
-(** This lemma is needed in fault_weight_state_sorted_subset **)
-Lemma Rminus_lt_r : forall r1 r2,
-  (0 <= r2)%R -> (r1 - r2 <= r1)%R.
-Proof.
-  intros.
-  rewrite <- Rplus_0_r.
-  unfold Rminus.
-  by apply Rplus_le_compat_l, Rge_le, Ropp_0_le_ge_contravar.
-Qed.
-
-Lemma Rminus_lt_r_strict : forall r1 r2,
-  (0 < r2)%R -> (r1 - r2 <= r1)%R.
-Proof.
-  intros.
-  rewrite <- Rplus_0_r.
-  unfold Rminus.
-  by apply Rplus_le_compat_l, Rge_le, Ropp_0_le_ge_contravar, Rlt_le.
-Qed.
-
 Lemma Rtotal_le_gt : forall x y,
   (x <= y)%R \/ (x > y)%R.
 Proof.
diff --git a/theories/VLSM/Lib/SortedLists.v b/theories/VLSM/Lib/SortedLists.v
index 0e5b435e..6adc3365 100644
--- a/theories/VLSM/Lib/SortedLists.v
+++ b/theories/VLSM/Lib/SortedLists.v
@@ -58,14 +58,6 @@ Fixpoint add_in_sorted_list_fn {A} (compare : A -> A -> comparison) (x : A) (l :
     end
   end.
 
-Lemma add_in_sorted_list_no_empty {A} (compare : A -> A -> comparison) : forall msg sigma,
-  add_in_sorted_list_fn compare msg sigma <> [].
-Proof.
-  unfold not. intros. destruct sigma; simpl in H.
-  - inversion H.
-  - destruct (compare msg a); inversion H.
-Qed.
-
 Lemma add_in_sorted_list_in {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} : forall msg msg' sigma,
   msg' ∈ (add_in_sorted_list_fn compare msg sigma) ->
   msg = msg' \/ msg' ∈ sigma.
@@ -176,24 +168,6 @@ Proof.
   - do 2 inversion 1; subst; firstorder.
 Qed.
 
-Lemma add_in_sorted_list_existing {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} : forall msg sigma,
-  LocallySorted (compare_lt compare) sigma ->
-  msg ∈ sigma ->
-  add_in_sorted_list_fn compare msg sigma = sigma.
-Proof.
-  induction sigma; intros.
-  - inversion H1.
-  - rewrite elem_of_cons in H1.
-    destruct H1 as [Heq | Hin].
-    + by subst; simpl; rewrite compare_eq_refl.
-    + apply LocallySorted_tl in H0 as LS.
-      spec IHsigma LS Hin. simpl.
-      destruct (compare msg a) eqn:Hcmp; try rewrite IHsigma. 1, 3: done.
-      apply (@LocallySorted_elem_of_lt _ _ compare_lt_strict_order msg a sigma H0) in Hin.
-      unfold compare_lt in Hin. apply compare_asymmetric in Hin.
-      rewrite Hin in Hcmp. inversion Hcmp.
-Qed.
-
 Lemma set_eq_first_equal {A}  {lt : relation A} `{StrictOrder A lt} :
   forall x1 x2 s1 s2,
   LocallySorted lt (x1 :: s1) ->
@@ -329,44 +303,3 @@ Proof.
   spec Hneed; [| done].
   apply elem_of_app; right; left.
 Qed.
-
-Lemma lsorted_pair_wise_unordered
-  {A : Type}
-  (l : list A)
-  (R : A -> A -> Prop)
-  (Hsorted : LocallySorted R l)
-  (Htransitive : Transitive R)
-  (x y : A)
-  (Hin_x : x ∈ l)
-  (Hin_y : y ∈ l) :
-  x = y \/ R x y \/ R y x.
-Proof.
-  apply elem_of_list_split in Hin_x.
-  destruct Hin_x as [pref1 [suf1 Hconcat1]].
-  rewrite Hconcat1 in Hin_y.
-  apply elem_of_app in Hin_y.
-  rewrite elem_of_cons in Hin_y.
-  assert (y =x \/ y ∈ (pref1 ++ suf1)). {
-    destruct Hin_y as [Hin_y|Hin_y]; [|destruct Hin_y].
-    - by right; apply elem_of_app; left.
-    - by left.
-    - by right; apply elem_of_app; right.
-  }
-  clear Hin_y.
-  rename H into Hin_y.
-  destruct Hin_y as [Hin_y|Hin_y].
-  - symmetry in Hin_y.
-    itauto.
-  - apply elem_of_app in Hin_y; destruct Hin_y.
-    * apply elem_of_list_split in H.
-      destruct H as [pref2 [suf2 Hconcat2]].
-      rewrite Hconcat2 in Hconcat1.
-      rewrite <- app_assoc in Hconcat1.
-      specialize (lsorted_pairwise_ordered l R Hsorted Htransitive y x pref2 suf2 suf1 Hconcat1).
-      by intros; right; right.
-    * apply elem_of_list_split in H.
-      destruct H as [pref2 [suf2 Hconcat2]].
-      rewrite Hconcat2 in Hconcat1.
-      specialize (lsorted_pairwise_ordered l R Hsorted Htransitive x y pref1 pref2 suf2 Hconcat1).
-      by intros; right; left.
-Qed.
diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v
index b1a62155..dbc702a8 100644
--- a/theories/VLSM/Lib/StdppExtras.v
+++ b/theories/VLSM/Lib/StdppExtras.v
@@ -229,38 +229,6 @@ Proof.
     destruct (decide (P a)); destruct (decide (Q a)); itauto.
 Qed.
 
-Lemma NoDup_elem_of_remove A (l l' : list A) a :
-  NoDup (l ++ a :: l') -> NoDup (l ++ l') /\ a ∉ (l ++ l').
-Proof.
-  intros Hnda.
-  apply NoDup_app in Hnda.
-  destruct Hnda as [Hnd [Ha Hnda]].
-  apply NoDup_cons in Hnda.
-  setoid_rewrite elem_of_cons in Ha.
-  destruct Hnda as [Ha' Hnd']; split.
-  - by apply NoDup_app; firstorder.
-  - by rewrite elem_of_app; firstorder.
-Qed.
-
-Lemma list_lookup_lt [A] (is : list A) :
-  forall i, is_Some (is !! i) ->
-  forall j, j < i -> is_Some (is !! j).
-Proof.
-  intros; apply lookup_lt_is_Some.
-  by etransitivity; [| apply lookup_lt_is_Some].
-Qed.
-
-Lemma list_suffix_lookup
-  {A : Type}
-  (s : list A)
-  (n : nat)
-  (i : nat)
-  (Hi : n <= i)
-  : list_suffix s n !! (i - n) = s !! i.
-Proof.
-  revert s n Hi; induction i; intros [| a s] [| n] Hi; cbn; try done; [| apply IHi]; lia.
-Qed.
-
 Lemma list_difference_singleton_not_in `{EqDecision A} :
   forall (l : list A) (a : A), a ∉ l ->
     list_difference l [a] = l.
@@ -285,27 +253,6 @@ Proof.
   - by inversion 1; subst; [done |]; cbn; spec IHl; [| lia].
 Qed.
 
-Lemma longer_subseteq_has_dups `{EqDecision A} :
-  forall l1 l2 : list A, l1 ⊆ l2 -> length l1 > length l2 ->
-  exists (i1 i2 : nat) (a : A), i1 ≠ i2 ∧ l1 !! i1 = Some a /\ l1 !! i2 = Some a.
-Proof.
-  induction l1; [inversion 2 |].
-  intros l2 Hl12 Hlen12.
-  destruct (decide (a ∈ l1)).
-  - exists 0.
-    apply elem_of_list_lookup_1 in e as [i2 Hi2].
-    by exists (S i2), a.
-  - edestruct (IHl1 (list_difference l2 [a]))
-           as (i1 & i2 & a' & Hi12 & Hli1 & Hli2); cycle 2.
-    + exists (S i1), (S i2), a'; cbn; itauto.
-    + intros x Hx.
-      rewrite elem_of_list_difference, elem_of_list_singleton.
-      by split; [apply Hl12; right | by contradict n; subst].
-    + cbn in Hlen12.
-      assert (Ha : a ∈ l2) by (apply Hl12; left).
-      specialize (list_difference_singleton_length_in _ _ Ha) as Hlen'; lia.
-Qed.
-
 Lemma ForAllSuffix2_lookup [A : Type] (R : A -> A -> Prop) l
   : ForAllSuffix2 R l <-> forall n a b, l !! n = Some a -> l !! (S n) = Some b -> R a b.
 Proof.
@@ -337,18 +284,6 @@ Proof.
   by transitivity c; [apply IHk | eapply Hall].
 Qed.
 
-(** If the <<n>>-th element of <<l>> is <<x>>, then we can decompose long enough
-    suffixes of <<l>> into <<x>> and a suffix shorter by 1. *)
-Lemma lastn_length_cons :
-  forall {A : Type} (n : nat) (l : list A) (x : A),
-    l !! n = Some x -> lastn (length l - n) l = x :: lastn (length l - S n) l.
-Proof.
-  intros A n l x H.
-  unfold lastn.
-  rewrite <- rev_length, <- !skipn_rev, rev_involutive.
-  by apply drop_S.
-Qed.
-
 Lemma filter_in {A} P `{∀ (x:A), Decision (P x)} x s :
   In x s ->
   P x ->
diff --git a/theories/VLSM/Lib/StreamExtras.v b/theories/VLSM/Lib/StreamExtras.v
index ba6624e6..b3bfdbd0 100644
--- a/theories/VLSM/Lib/StreamExtras.v
+++ b/theories/VLSM/Lib/StreamExtras.v
@@ -49,14 +49,6 @@ Qed.
 
 Definition ForAll1 [A : Type] (P : A -> Prop) := ForAll (fun s => P (hd s)).
 
-Lemma ForAll1_subsumption [A:Type] (P Q: A -> Prop)
-  (HPQ : forall a, P a -> Q a)
-  : forall s, ForAll1 P s -> ForAll1 Q s.
-Proof.
-  apply ForAll_subsumption.
-  intro s. apply HPQ.
-Qed.
-
 Lemma ForAll1_forall [A : Type] (P : A -> Prop) s
   : ForAll1 P s <-> forall n, P (Str_nth n s).
 Proof.
@@ -124,17 +116,6 @@ Proof.
   by induction l; cbn; f_equal.
 Qed.
 
-Lemma stream_app_f_equal
-  {A : Type}
-  (l1 l2 : list A)
-  (s1 s2 : Stream A)
-  (Hl : l1 = l2)
-  (Hs : EqSt s1 s2)
-  : EqSt (stream_app l1 s1) (stream_app l2 s2).
-Proof.
-  by subst; induction l2; [ | constructor].
-Qed.
-
 Lemma stream_app_inj_l
   {A : Type}
   (l1 l2 : list A)
@@ -248,35 +229,6 @@ Proof.
       right. apply IHn. exists k. split; [lia | done].
 Qed.
 
-Lemma stream_prefix_app_l
-  {A : Type}
-  (l : list A)
-  (s : Stream A)
-  (n : nat)
-  (Hle : n <= length l)
-  : stream_prefix (stream_app l s) n = list_prefix l n.
-Proof.
-  revert n Hle; induction l; intros [| n] Hle.
-  1-3: by inversion Hle.
-  by cbn in *; rewrite IHl; [| lia].
-Qed.
-
-Lemma stream_prefix_app_r
-  {A : Type}
-  (l : list A)
-  (s : Stream A)
-  (n : nat)
-  (Hge : n >= length l)
-  : stream_prefix (stream_app l s) n = l ++ stream_prefix s (n - length l).
-Proof.
-  generalize dependent l.
-  generalize dependent s.
-  induction n.
-  - intros s [| a l] Hge; cbn in *; [done | lia].
-  - intros s [| a l] Hge; cbn in *; [done |].
-    rewrite <- IHn; [done | lia].
-Qed.
-
 Lemma stream_prefix_map
   {A B : Type}
   (f : A -> B)
@@ -301,29 +253,6 @@ element or two consecutive elements at a time with corresponding list
 quantifiers applied on their finite prefixes.
 *)
 
-Lemma stream_prefix_ForAll
-  {A : Type}
-  (P : A -> Prop)
-  (s : Stream A)
-  : ForAll1 P s <-> forall n : nat, Forall P (stream_prefix s n).
-Proof.
-  rewrite ForAll1_forall.
-  setoid_rewrite (Forall_nth P (hd s)).
-  setoid_rewrite stream_prefix_length.
-  specialize (stream_prefix_nth s) as Hi.
-  split.
-  - intros Hp n i Hlt.
-    specialize (Hi _ _ Hlt).
-    apply nth_error_nth with (d := hd s) in Hi.
-    rewrite Hi. apply Hp.
-  - intros Hp n.
-    assert (Hn : n < S n) by lia.
-    specialize (Hp _ _ Hn).
-    specialize (Hi _ _ Hn).
-    apply nth_error_nth with (d := hd s) in Hi.
-    by rewrite Hi in Hp.
-Qed.
-
 Lemma stream_prefix_ForAll2
   {A : Type}
   (R : A -> A -> Prop)
@@ -369,37 +298,6 @@ Proof.
     by apply Hp.
 Qed.
 
-Lemma ForAll2_strict_lookup_rev [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R}
-  (l : Stream A) (Hl : ForAll2 R l)
-  : forall m n, R (Str_nth m l) (Str_nth n l) -> m < n.
-Proof.
-  intros m n Hr.
-  destruct (decide (n <= m)); [|lia].
-  exfalso.
-  destruct HR as [HI HT].
-  rewrite ForAll2_transitive_lookup in Hl by done.
-  destruct (decide (m = n)); subst.
-  - by elim (HI (Str_nth n l)).
-  - specialize (Hl n m). spec Hl; [lia|].
-    elim (HI (Str_nth n l)).
-    by transitivity (Str_nth m l).
-Qed.
-
-Lemma ForAll2_strict_lookup_inj
- [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R}
-  (l : Stream A) (Hl : ForAll2 R l)
-  : forall m n, Str_nth m l = Str_nth n l -> m = n.
-Proof.
-  intros m n Hmn.
-  destruct HR as [HI HT].
-  rewrite ForAll2_transitive_lookup in Hl by done.
-  destruct (decide (m = n)); [done |].
-  elim (HI (Str_nth n l)).
-  by destruct (decide (m < n))
-  ; [spec Hl m n|spec Hl n m]; (spec Hl; [lia|])
-  ; rewrite Hmn in Hl.
-Qed.
-
 Definition stream_suffix
   {A : Type}
   (l : Stream A)
@@ -407,17 +305,6 @@ Definition stream_suffix
   : Stream A
   := Str_nth_tl n l.
 
-Lemma stream_suffix_S
-  {A : Type}
-  (l : Stream A)
-  (n : nat)
-  : stream_suffix l n = Cons (Str_nth n l) (stream_suffix l (S n)).
-Proof.
-  revert l. induction n; intros.
-  - by destruct l.
-  - by apply IHn.
-Qed.
-
 Lemma stream_suffix_nth
   {A : Type}
   (s : Stream A)
@@ -459,21 +346,6 @@ Definition stream_segment
   : list A
   := list_suffix (stream_prefix l n2) n1.
 
-Lemma stream_segment_nth
-  {A : Type}
-  (l : Stream A)
-  (n1 n2 : nat)
-  (Hn : n1 <= n2)
-  (i : nat)
-  (Hi1 : n1 <= i)
-  (Hi2 : i < n2)
-  : nth_error (stream_segment l n1 n2) (i - n1) = Some (Str_nth i l).
-Proof.
-  unfold stream_segment.
-  rewrite list_suffix_nth; [| done].
-  by apply stream_prefix_nth.
-Qed.
-
 Definition stream_segment_alt
   {A : Type}
   (l : Stream A)
@@ -481,31 +353,6 @@ Definition stream_segment_alt
   : list A
   := stream_prefix (stream_suffix l n1) (n2 - n1).
 
-Lemma stream_segment_alt_iff
-  {A : Type}
-  (l : Stream A)
-  (n1 n2 : nat)
-  : stream_segment l n1 n2 = stream_segment_alt l n1 n2.
-Proof.
-  apply nth_error_eq.
-  intro k.
-  unfold stream_segment_alt. unfold stream_segment.
-  destruct (decide (n2 - n1 <= k)).
-  - specialize (nth_error_None (list_suffix (stream_prefix l n2) n1) k); intros [_ H].
-    specialize (nth_error_None (stream_prefix (stream_suffix l n1) (n2 - n1)) k); intros [_ H_alt].
-    rewrite H, H_alt; [done | |].
-    + by rewrite stream_prefix_length.
-    + by rewrite list_suffix_length, stream_prefix_length.
-  - rewrite stream_prefix_nth, stream_suffix_nth by lia.
-    assert (Hle : n1 <= n1 + k) by lia.
-    specialize (list_suffix_nth (stream_prefix l n2) n1 (n1 + k) Hle)
-    ; intro Heq.
-    clear Hle.
-    assert (Hs: n1 + k - n1 = k) by lia.
-    rewrite Hs in Heq.
-    rewrite Heq, stream_prefix_nth; [do 2 f_equal |]; lia.
-Qed.
-
 Lemma stream_prefix_segment
   {A : Type}
   (l : Stream A)
@@ -535,31 +382,6 @@ Proof.
   by rewrite stream_prefix_segment.
 Qed.
 
-Lemma stream_segment_app
-  {A : Type}
-  (l : Stream A)
-  (n1 n2 n3 : nat)
-  (H12 : n1 <= n2)
-  (H23 : n2 <= n3)
-  : stream_segment l n1 n2 ++ stream_segment l n2 n3 = stream_segment l n1 n3.
-Proof.
-  assert (Hle : n1 <= n3) by lia.
-  specialize (stream_prefix_segment_suffix l n1 n3 Hle); intro Hl1.
-  specialize (stream_prefix_segment_suffix l n2 n3 H23); intro Hl2.
-  rewrite <- Hl2 in Hl1 at 4. clear Hl2.
-  apply stream_app_inj_l in Hl1.
-  - specialize (list_prefix_suffix (stream_prefix l n2) n1); intro Hl2.
-    specialize (stream_prefix_prefix l n1 n2 H12); intro Hl3.
-    rewrite Hl3 in Hl2.
-    rewrite <- Hl2, <- app_assoc in Hl1.
-    by apply app_inv_head in Hl1.
-  - repeat rewrite app_length.
-    unfold stream_segment.
-    repeat rewrite list_suffix_length.
-    repeat rewrite stream_prefix_length.
-    lia.
-Qed.
-
 Definition monotone_nat_stream_prop
   (s : Stream nat)
   := forall n1 n2 : nat, n1 < n2 -> Str_nth n1 s < Str_nth n2 s.
@@ -599,20 +421,6 @@ Proof.
     spec Hs; lia.
 Qed.
 
-Definition monotone_nat_stream :=
-  {s : Stream nat | monotone_nat_stream_prop s}.
-
-Lemma monotone_nat_stream_tl
-  (s : Stream nat)
-  (Hs : monotone_nat_stream_prop s)
-  : monotone_nat_stream_prop (tl s).
-Proof.
-  intros n1 n2 Hlt.
-  specialize (Hs (S n1) (S n2)).
-  apply Hs.
-  lia.
-Qed.
-
 CoFixpoint nat_sequence_from (n : nat) : Stream nat
   := Cons n (nat_sequence_from (S n)).
 
@@ -638,9 +446,6 @@ Proof.
   apply ForAll2_forall. intro m. rewrite !nat_sequence_from_nth. lia.
 Qed.
 
-Definition nat_sequence_sorted : ForAll2 lt nat_sequence :=
-  nat_sequence_from_sorted 0.
-
 Lemma nat_sequence_from_prefix_sorted
   : forall m n, LocallySorted lt (stream_prefix (nat_sequence_from m) n).
 Proof.
@@ -694,18 +499,6 @@ Definition FinitelyMany : Stream A -> Prop :=
 Definition FinitelyManyBound (s : Stream A) : Type :=
   { n : nat | ForAll1 (fun a => ~ P a) (Str_nth_tl n s)}.
 
-Lemma FinitelyMany_from_bound
-  : forall s, FinitelyManyBound s -> FinitelyMany s.
-Proof.
-  intros s [n Hn].
-  apply Exists_Str_nth_tl.
-  by exists n.
-Qed.
-
-Lemma InfinitelyOften_tl s
-  : InfinitelyOften s -> InfinitelyOften (tl s).
-Proof. by inversion 1. Qed.
-
 Definition InfinitelyOften_nth_tl
   : forall n s, InfinitelyOften s -> InfinitelyOften (Str_nth_tl n s)
   := (@ForAll_Str_nth_tl _ (Exists1 P)).
diff --git a/theories/VLSM/Lib/StreamFilters.v b/theories/VLSM/Lib/StreamFilters.v
index d70f59d4..2b5db905 100644
--- a/theories/VLSM/Lib/StreamFilters.v
+++ b/theories/VLSM/Lib/StreamFilters.v
@@ -41,19 +41,6 @@ Proof.
   by apply filtering_subsequence_sorted in Hfs.
 Qed.
 
-Lemma filtering_subsequence_iff
-  {A : Type}
-  (P Q : A -> Prop)
-  (HPQ : forall a, P a <-> Q a)
-  (s : Stream A)
-  (ss : Stream nat)
-  : filtering_subsequence P s ss <-> filtering_subsequence Q s ss.
-Proof.
-  unfold filtering_subsequence.
-  rewrite !ForAll2_forall.
-  by setoid_rewrite <- HPQ.
-Qed.
-
 (** Each element in a [filtering_subsequence] is a position in the base
 stream for which the predicate holds.
 *)
@@ -276,23 +263,6 @@ Next Obligation.
   by apply filtering_subsequence_prefix_length.
 Qed.
 
-Lemma stream_filter_Forall
-  {A : Type}
-  (P : A -> Prop)
-  (s : Stream A)
-  (ss : Stream nat)
-  (s' := stream_subsequence s ss)
-  (Hfs : filtering_subsequence P s ss)
-  : ForAll1 P s'.
-Proof.
-  apply ForAll1_forall.
-  intro n.
-  unfold s'.
-  unfold stream_subsequence.
-  rewrite Str_nth_map.
-  by apply filtering_subsequence_witness.
-Qed.
-
 (** ** Obtaining [filtering_sequences] for streams
 
 Given a stream, a decidable predicate on its elements, and a guarantee that the
@@ -383,28 +353,6 @@ Proof.
   rewrite Heq. simpl. lia.
 Qed.
 
-Lemma stream_filter_fst_pos_nth_tl_has_property
-  (s : Stream A)
-  (n : nat)
-  (sn := Str_nth_tl n s)
-  (Hev : Exists1 P sn)
-  (fpair := stream_filter_fst_pos (Str_nth_tl n s) Hev n)
-  : P (Str_nth fpair.1 s) /\
-    forall i, n <= i < fpair.1 -> ~ P (Str_nth i s).
-Proof.
-  specialize (stream_filter_fst_pos_characterization sn Hev n)
-    as [k [Heq [Hp Hnp]]].
-  subst sn fpair.
-  rewrite Heq.
-  clear -Hp Hnp. rewrite Str_nth_plus, Nat.add_comm in Hp.
-  split; [done |].
-  intros i [Hlt_i Hilt].
-  apply le_plus_dec in Hlt_i as [i' Hi].
-  subst i.
-  rewrite <- Str_nth_plus.
-  apply Hnp. simpl in *. lia.
-Qed.
-
 (** Given as stream <<s>> for which predicate <<P>> holds [InfinitelyOften]
 produces the streams of all its position at which <<P>> holds in a strictly
 increasing order (shifted by the given argument <<n>>).
@@ -463,18 +411,6 @@ Proof.
     replace (n0 + S (k + kn)) with (S (n0 + kn + k)) by lia. eauto.
 Qed.
 
-Lemma stream_filter_positions_monotone
-  (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat)
-  : monotone_nat_stream_prop (stream_filter_positions s Hinf n).
-Proof.
-  apply monotone_nat_stream_prop_from_successor.
-  revert s Hinf n.
-  cofix H.
-  intros.
-  constructor; simpl; [|apply H].
-  apply stream_filter_fst_pos_le.
-Qed.
-
 (** [stream_filter_positions] produces a [filtering_sequence].
 *)
 Lemma stream_filter_positions_filtering_subsequence
@@ -517,14 +453,6 @@ Definition stream_filter_map
   : Stream B :=
   filtering_subsequence_stream_filter_map P f _ _ (stream_filter_positions_filtering_subsequence s Hinf).
 
-(** Stream filtering is obtained as a specialization of [stream_filter_map].
-*)
-Definition stream_filter
-  (s : Stream A)
-  (Hinf : InfinitelyOften P s)
-  : Stream A :=
-  stream_filter_map proj1_sig s Hinf.
-
 End stream_filter_positions.
 
 Section stream_map_option.
@@ -547,18 +475,6 @@ Definition stream_map_option
   : Stream B :=
   stream_filter_map P (fun k : dsig P => is_Some_proj (proj2_dsig k)) s Hinf.
 
-Lemma stream_map_option_prefix
-  (Hinf : InfinitelyOften P s)
-  (n : nat)
-  (map_opt_pre := map_option f (stream_prefix s n))
-  (m := length map_opt_pre)
-  : stream_prefix (stream_map_option Hinf) m = map_opt_pre.
-Proof.
-  subst map_opt_pre m.
-  rewrite !(map_option_as_filter f (stream_prefix s n)).
-  apply fitering_subsequence_stream_filter_map_prefix.
-Qed.
-
 Program Definition stream_map_option_prefix_ex
   (Hinf : InfinitelyOften P s)
   (Hfs := stream_filter_positions_filtering_subsequence _ _ Hinf)
@@ -570,11 +486,6 @@ Next Obligation.
   by intros; cbn; rewrite !map_option_as_filter.
 Qed.
 
-Definition bounded_stream_map_option
-  (Hfin : FinitelyManyBound P s)
-  : list B :=
-  map_option f (stream_prefix s (` Hfin)).
-
 End stream_map_option.
 
 (** For a totally defined function, [stream_map_option] corresponds to the
diff --git a/theories/VLSM/Lib/Temporal.v b/theories/VLSM/Lib/Temporal.v
index 2b209209..d575f48f 100644
--- a/theories/VLSM/Lib/Temporal.v
+++ b/theories/VLSM/Lib/Temporal.v
@@ -116,19 +116,6 @@ Lemma refutation [A:Type] [R:A -> A-> Prop] (HR: well_founded R)
   by eapply H0; eauto.
 Qed.
 
-Lemma forall_forever: forall [A B:Type] (P: A -> Stream B -> Prop) [s: Stream B],
-    (forall (a:A), Forever (P a) s) -> Forever (fun s => forall a, P a s) s.
-Proof.
-  intros A B P.
-  cofix forall_forever.
-  destruct s.
-  intro H.
-  constructor.
-  - intro a. by destruct (H a).
-  - apply forall_forever.
-    intro a. by destruct (H a).
-Qed.
-
 Lemma not_forever [A:Type] (P: Stream A -> Prop):
   forall s, ~Forever P s -> Eventually (fun s => ~ P s) s.
 Proof.
diff --git a/theories/VLSM/Lib/TopSort.v b/theories/VLSM/Lib/TopSort.v
index 60a9a663..902a93f7 100644
--- a/theories/VLSM/Lib/TopSort.v
+++ b/theories/VLSM/Lib/TopSort.v
@@ -336,10 +336,6 @@ Proof.
   right; left.
 Qed.
 
-(**
-As a corollary of the above, if <<a precedes b>> then <<a>> can be found before
-<<b>> in l.
-*)
 Corollary top_sort_precedes
   (a b : A)
   (Hab : precedes a b)