Comment out wf_splice_list

It wasn't actually ready yet

1 files changed, 2 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v
index bc97dd809..ba4e0aa2c 100644
--- a/src/Experiments/NewPipeline/UnderLetsProofs.v
+++ b/src/Experiments/NewPipeline/UnderLetsProofs.v
@@ -232,6 +232,7 @@ Module Compilers.
           eauto using (ex_intro _ nil).
         Qed.
 
+        (*
         Lemma wf_splice_list {A1 B1 A2 B2}
               {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop}
               {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop}
@@ -250,6 +251,7 @@ Module Compilers.
           rewrite ListUtil.app_cons_app_app in *.
           eauto using (ex_intro _ nil).
         Qed.
+         *)
       End with_var.
     End with_ident.