Add reflect_list_cps_id

1 files changed, 4 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v
index d00efa46c..825881771 100644
--- a/src/Experiments/NewPipeline/LanguageInversion.v
+++ b/src/Experiments/NewPipeline/LanguageInversion.v
@@ -558,6 +558,10 @@ Module Compilers.
         apply reflect_list_cps'_id_cons_body; assumption.
       Qed.
 
+      Lemma reflect_list_cps_id {t} {e : expr (base.type.list t)}
+        : forall T k, @invert_expr.reflect_list_cps _ _ e T k = k (invert_expr.reflect_list e).
+      Proof. exact (@reflect_list_cps'_id _ e). Qed.
+
       Lemma reflect_list_step {t} {e : expr (base.type.list t)}
         : invert_expr.reflect_list e
           = match invert_expr.invert_nil e, invert_expr.invert_cons e with