Fix an issue with a proof from the previous commit

Also move lam_type_of_list to Rewriter (in prep for reifying rewrite
rules).

1 files changed, 7 insertions, 0 deletions

diff --git a/src/Rewriter.v b/src/Rewriter.v
index e23b65ae7..06f8d59fe 100644
--- a/src/Rewriter.v
+++ b/src/Rewriter.v
@@ -506,6 +506,13 @@ Module Compilers.
                ls
                f args.
 
+        Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls
+          := list_rect
+               (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls)
+               (fun f => f tt)
+               (fun T Ts rec k t => rec (fun ts => k (t, ts)))
+               ls.
+
         Local Notation "e <---- e' ; f" := (splice_value_with_lets e' (fun e => f%under_lets)) : under_lets_scope.
         Local Notation "e <----- e' ; f" := (splice_under_lets_with_value e' (fun e => f%under_lets)) : under_lets_scope.