1 files changed, 1 insertions, 33 deletions
diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index 4e5c79cae..978c49189 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -19,6 +19,7 @@ Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.ForallIn.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.HProp.
@@ -190,39 +191,6 @@ Module Compilers.
             (nat_rect (fun _ => @Compile.value base.type ident var2 (type.base A -> type.base B)) O2 S2 n).
       Proof. induction n; cbn [nat_rect]; auto. Qed.
 
-      (** TODO: MOVE ME? *)
-      Lemma fold_right_impl_Proper {A} {P Q : A -> Prop} ls (concl1 concl2 : Prop)
-            (Hconcl : concl1 -> concl2)
-            (HPQ : forall a, In a ls -> Q a -> P a)
-        : fold_right (fun a (concl : Prop) => P a -> concl) concl1 ls
-          -> fold_right (fun a (concl : Prop) => Q a -> concl) concl2 ls.
-      Proof. induction ls as [|x xs IHxs]; cbn [fold_right In] in *; intuition. Qed.
-
-      Lemma forall_In_existT {A P} {Q : forall a : A, P a -> Prop} ls
-        : fold_right
-            (fun xp (concl : Prop)
-             => Q (projT1 xp) (projT2 xp) -> concl)
-            (forall x p, In (@existT A P x p) ls -> Q x p)
-            ls.
-      Proof.
-        induction ls as [|x xs IHxs]; cbn [fold_right In]; intros;
-          destruct_head' False; destruct_head'_or.
-        eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (subst; eauto).
-      Qed.
-
-      (** TODO: MOVE ME? *)
-      Lemma forall_In_pair_existT {A A' P P'} {Q : forall (a : A) (a' : A'), P a -> P' a' -> Prop} ls
-        : fold_right
-            (fun xp_x'p' (concl : Prop)
-             => Q (projT1 (fst xp_x'p')) (projT1 (snd xp_x'p')) (projT2 (fst xp_x'p')) (projT2 (snd xp_x'p')) -> concl)
-            (forall x p x' p', In (@existT A P x p, @existT A' P' x' p') ls -> Q x x' p p')
-            ls.
-      Proof.
-        induction ls as [|x xs IHxs]; cbn [fold_right In]; intros;
-          destruct_head' False; destruct_head'_prod; destruct_head'_or; intros.
-        eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto).
-      Qed.
-
       Local Ltac start_good :=
         split; [ reflexivity | ];
         lazymatch goal with