Fix an issue with a proof from the previous commit

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

2 files changed, 8 insertions, 7 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.
 
diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v
index 0ec6396f2..49af85a60 100644
--- a/src/RewriterWf1.v
+++ b/src/RewriterWf1.v
@@ -65,6 +65,7 @@ Module Compilers.
         Proof using Type.
           revert t; induction pt;
             repeat first [ progress cbn [pattern.base.subst pattern.base.subst_default]
+                         | progress cbv [pattern.base.lookup_default]
                          | progress cbv [Option.bind option_map]
                          | progress inversion_option
                          | progress subst
@@ -895,13 +896,6 @@ Module Compilers.
         Local Notation unification_resultT' := (@unification_resultT' pident pident_arg_types).
         Local Notation unification_resultT := (@unification_resultT pident pident_arg_types).
 
-        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.
-
         Lemma app_lam_type_of_list
               {K ls f args}
           : @app_type_of_list K ls (@lam_type_of_list ls K f) args = f args.