From a4cd12c5726818ed1f155ab79904ef0de5f9a815 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 6 Jun 2024 18:38:53 +0200
Subject: [PATCH] Add the force (lazy t) evaluation rule to lambda-box

---
 erasure-plugin/theories/ETransform.v          |  2 +-
 erasure/theories/EAstUtils.v                  | 11 ++++
 erasure/theories/EConstructorsAsBlocks.v      | 36 +++++++++++-
 erasure/theories/EDeps.v                      |  1 +
 erasure/theories/EEtaExpandedFix.v            |  5 +-
 erasure/theories/EImplementBox.v              | 13 +++++
 erasure/theories/EInlineProjections.v         |  7 ++-
 erasure/theories/EOptimizePropDiscr.v         |  6 +-
 erasure/theories/ERemoveParams.v              | 14 ++++-
 erasure/theories/EWcbvEval.v                  | 33 ++++++-----
 .../EWcbvEvalCstrsAsBlocksFixLambdaInd.v      | 22 ++++++--
 erasure/theories/EWcbvEvalCstrsAsBlocksInd.v  | 24 ++++++--
 erasure/theories/EWcbvEvalEtaInd.v            | 51 +++++++++++------
 erasure/theories/EWcbvEvalInd.v               |  9 ++-
 erasure/theories/EWcbvEvalNamed.v             | 55 +++++++++++++++----
 erasure/theories/ErasureCorrectness.v         | 12 ++++
 erasure/theories/Typed/OptimizeCorrectness.v  | 20 ++++---
 erasure/theories/Typed/WcbvEvalAux.v          |  1 +
 18 files changed, 249 insertions(+), 73 deletions(-)

diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v
index 3af3e47a8..06a08372a 100644
--- a/erasure-plugin/theories/ETransform.v
+++ b/erasure-plugin/theories/ETransform.v
@@ -976,7 +976,7 @@ Program Definition coinductive_to_inductive_transformation (efl : EEnvFlags)
   {has_cstrblocks : cstr_as_blocks = true} :
   Transform.t _ _ EAst.term EAst.term _ _
     (eval_eprogram_env block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
-  {| name := "transforming co-inductive to inductive types";
+  {| name := "transforming co-inductive to lazy inductive types";
     transform p _ := ECoInductiveToInductive.trans_program p ;
     pre p := wf_eprogram_env efl p ;
     post p := wf_eprogram efl p ;
diff --git a/erasure/theories/EAstUtils.v b/erasure/theories/EAstUtils.v
index de7c2655c..4f3403da3 100644
--- a/erasure/theories/EAstUtils.v
+++ b/erasure/theories/EAstUtils.v
@@ -318,9 +318,16 @@ Definition is_box c :=
   | _ => false
   end.
 
+Definition isLazy c :=
+  match c with
+  | tLazy _ => true
+  | _ => false
+  end.
+
 Definition isFixApp t := isFix (head t).
 Definition isConstructApp t := isConstruct (head t).
 Definition isPrimApp t := isPrim (head t).
+Definition isLazyApp t := isLazy (head t).
 
 Lemma isFixApp_mkApps f l : isFixApp (mkApps f l) = isFixApp f.
 Proof. rewrite /isFixApp head_mkApps //. Qed.
@@ -328,6 +335,8 @@ Lemma isConstructApp_mkApps f l : isConstructApp (mkApps f l) = isConstructApp f
 Proof. rewrite /isConstructApp head_mkApps //. Qed.
 Lemma isPrimApp_mkApps f l : isPrimApp (mkApps f l) = isPrimApp f.
 Proof. rewrite /isPrimApp head_mkApps //. Qed.
+Lemma isLazyApp_mkApps f l : isLazyApp (mkApps f l) = isLazyApp f.
+Proof. rewrite /isLazyApp head_mkApps //. Qed.
 
 Lemma is_box_mkApps f a : is_box (mkApps f a) = is_box f.
 Proof.
@@ -347,6 +356,8 @@ Lemma nisBox_mkApps f args : ~~ isBox f -> ~~ isBox (mkApps f args).
 Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
 Lemma nisPrim_mkApps f args : ~~ isPrim f -> ~~ isPrim (mkApps f args).
 Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
+Lemma nisLazy_mkApps f args : ~~ isLazy f -> ~~ isLazy (mkApps f args).
+Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
 
 Definition string_of_def {A : Set} (f : A -> string) (def : def A) :=
   "(" ^ string_of_name (dname def) ^ "," ^ f (dbody def) ^ ","
diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
index 0032bef87..c4453bbae 100644
--- a/erasure/theories/EConstructorsAsBlocks.v
+++ b/erasure/theories/EConstructorsAsBlocks.v
@@ -649,6 +649,28 @@ Proof.
     eapply IHt1. cbn in Hwf'. rtoProp. intuition.
 Qed.
 
+Lemma transform_blocks_isLazyApp {efl : EEnvFlags} {Σ : GlobalContextMap.t} t :
+  has_cstr_params = false ->
+  wf_glob Σ -> wellformed Σ 0 t ->
+  isLazyApp (transform_blocks Σ t) = isLazyApp t.
+Proof.
+  intros haspars Hwf Hwf'.
+  induction t; try now cbn; eauto.
+  eapply transform_blocks_tApp; eauto.
+  destruct decompose_app.
+  destruct construct_viewc.
+  - rewrite GlobalContextMap.lookup_constructor_pars_args_spec.
+    destruct lookup_constructor_pars_args as [ [[]] | ]; eauto.
+    cbn. destruct chop. intros (? & ? & ?). subst.
+    rewrite -[tApp _ _](mkApps_app _ _ [t2]).
+    rewrite !isLazyApp_mkApps. cbn. reflexivity.
+  - change (tApp t1 t2) with (mkApps t1 [t2]).
+    change (tApp (transform_blocks Σ t1) (transform_blocks Σ t2)) with
+    (mkApps (transform_blocks Σ t1) [transform_blocks Σ t2]).
+    rewrite !isLazyApp_mkApps.
+    eapply IHt1. cbn in Hwf'. rtoProp. intuition.
+Qed.
+
 Lemma lookup_env_transform_blocks {Σ : GlobalContextMap.t} kn :
   lookup_env (transform_blocks_env Σ) kn =
   option_map (transform_blocks_decl Σ) (lookup_env Σ kn).
@@ -1125,17 +1147,20 @@ Proof.
       * rewrite GlobalContextMap.lookup_constructor_pars_args_spec;
           destruct lookup_constructor_pars_args as [ [[]] | ] eqn:hpa; eauto.
         cbn [plus]. destruct chop eqn:heqch.
-        intros [hl [ht ha]]. rewrite ht in H1. rewrite isConstructApp_mkApps isPrimApp_mkApps orb_true_r in H1 => //.
+        intros [hl [ht ha]]. rewrite ht in H1. rewrite isConstructApp_mkApps
+          isPrimApp_mkApps isLazyApp_mkApps orb_true_r in H1 => //.
       * eapply eval_app_cong; eauto.
         revert H1.
         destruct f'; try now cbn; tauto.
         intros H. cbn in H.
         rewrite transform_blocks_isConstructApp; eauto.
         rewrite transform_blocks_isPrimApp; eauto.
-        rewrite negb_or in H. move/andP: H => [] ncstr nprim.
+        rewrite transform_blocks_isLazyApp; eauto.
+        rewrite !negb_or in H. move/andP: H => [] /andP [] ncstr nprim nlazy.
         destruct (isConstructApp (tApp f'1 f'2)) eqn:heq'.
         -- cbn in ncstr. congruence.
-        -- eapply transform_blocks_tApp; eauto. clear -nprim.
+        -- eapply transform_blocks_tApp; eauto. clear -nprim nlazy.
+          move/negbTE: nlazy ->. move/negbTE: nprim -> => /=.
            destruct decompose_app.
            destruct construct_viewc; try now cbn; eauto.
            rewrite GlobalContextMap.lookup_constructor_pars_args_spec;
@@ -1186,6 +1211,11 @@ Proof.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. eapply All2_All2_Set. solve_all.
     now destruct b.
     now destruct a0.
+  - intros evl evt' [evt wft wflt etat etalt].
+    intros [evt'' wft' wfv etat' etav].
+    simp transform_blocks; rewrite -!transform_blocks_equation_1.
+    econstructor; eauto.
+    now simp transform_blocks in evt; rewrite -!transform_blocks_equation_1 in evt.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
     cbn -[lookup_constructor] in H |- *. destruct args => //.
     destruct lookup_constructor eqn:hl => //.
diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v
index b1180b5cc..7bee22452 100644
--- a/erasure/theories/EDeps.v
+++ b/erasure/theories/EDeps.v
@@ -354,6 +354,7 @@ Proof.
   - depelim er; depelim X; constructor; eauto.
     eapply All2_over_undep in a0. solve_all.
   - easy.
+  - easy.
 Qed.
 
 #[global]
diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
index a094a3021..f0a877898 100644
--- a/erasure/theories/EEtaExpandedFix.v
+++ b/erasure/theories/EEtaExpandedFix.v
@@ -1056,7 +1056,7 @@ Lemma eval_etaexp {fl : WcbvFlags} {efl : EEnvFlags} {wcon : with_constructor_as
 Proof.
   intros etaΣ wfΣ.
   induction 1 as [ | ? ? ? ? ? ? ? ? IHs | | | | | ? ? ? ? ? ? ? ? ? ? ? IHs | ? ? ? ? ? ? ? ? ? ? ? IHs
-    | ? ? ? ? ? ? ? ? ? ? IHs | | | | | | | | | | | ] using eval_mkApps_rect; try now congruence.
+    | ? ? ? ? ? ? ? ? ? ? IHs | | | | | | | | | | | | ] using eval_mkApps_rect; try now congruence.
   all:try simp isEtaExp; rewrite -?isEtaExp_equation_1 => //.
   6:{
     move/isEtaExp_tApp'.
@@ -1375,6 +1375,7 @@ Proof.
   - solve_all.
     depelim X; solve_all. eapply All2_over_undep in a. subst a0 a';
       depelim H; constructor; solve_all. solve_all.
+  - simp_eta in IHeval1. eauto.
 Qed.
 
 Lemma isEtaExp_fixapp_mon {mfix idx n n'} : n <= n' -> isEtaExp_fixapp mfix idx n -> isEtaExp_fixapp mfix idx n'.
@@ -1961,6 +1962,8 @@ Proof.
   - intros hexp. simp_eta in hexp. depelim X; repeat constructor; eauto.
     eapply All2_over_undep in a. subst a0 a'. solve_all. depelim hexp; cbn in *. destruct p.
     eapply All2_All2_Set. solve_all. solve_all. depelim hexp. destruct p. solve_all.
+  - intros hexp. simp_eta in hexp. econstructor; eauto. apply IHeval2.
+    specialize (IHeval1 hexp). eapply eval_etaexp in IHeval1. now simp_eta in IHeval1. all:eauto.
   - intros hexp. now eapply eval_atom.
     Unshelve. all: eauto.
 Qed.
diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
index 99deb0a5f..0817566d3 100644
--- a/erasure/theories/EImplementBox.v
+++ b/erasure/theories/EImplementBox.v
@@ -388,6 +388,15 @@ Proof.
   rewrite (isPrimApp_mkApps _ [_]). eauto.
 Qed.
 
+Lemma implement_box_isLazyApp {efl : EEnvFlags} {Σ : global_declarations} t :
+  isLazyApp (implement_box t) = isLazyApp t.
+Proof.
+  induction t; try now cbn; eauto.
+  simp implement_box.
+  rewrite (isLazyApp_mkApps _ [t2]).
+  rewrite (isLazyApp_mkApps _ [_]). eauto.
+Qed.
+
 Lemma lookup_env_implement_box {Σ : global_declarations} kn :
   lookup_env (implement_box_env Σ) kn =
   option_map (implement_box_decl) (lookup_env Σ kn).
@@ -670,6 +679,7 @@ Proof.
     intros H. cbn in H.
     rewrite implement_box_isConstructApp; eauto.
     rewrite implement_box_isPrimApp; eauto.
+    rewrite implement_box_isLazyApp; eauto.
   - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end.
     simp implement_box in *.
     eapply eval_construct_block; tea. eauto.
@@ -680,6 +690,9 @@ Proof.
   - intros wf H; depelim H; simp implement_box; repeat constructor.
     destruct a0. eapply All2_over_undep in a. eapply All2_All2_Set, All2_map.
     cbn -[implement_box]. solve_all. now destruct H. now destruct a0.
+  - intros evt evt' [] [].
+    simp implement_box. simp implement_box in e.
+    econstructor; eauto.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
     cbn -[lookup_constructor] in H |- *. destruct args => //.
 Qed.
diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v
index a37b97ae7..302b57bc3 100644
--- a/erasure/theories/EInlineProjections.v
+++ b/erasure/theories/EInlineProjections.v
@@ -710,13 +710,14 @@ Proof.
     * destruct with_guarded_fix.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps
+          !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         rewrite !andb_true_r.
         rtoProp; intuition auto;  destruct v => /= //.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
   - intros; rtoProp; intuition eauto.
@@ -725,6 +726,8 @@ Proof.
     eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp.
     subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all.
     primProp; depelim H0; intuition eauto.
+  - intros wf; econstructor; eauto. eapply IHev2.
+    eapply eval_wellformed in ev1; tea => //.
   - destruct t => //.
     all:constructor; eauto.
     cbn [atom optimize] in i |- *.
diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
index 211562f18..449e36dc8 100644
--- a/erasure/theories/EOptimizePropDiscr.v
+++ b/erasure/theories/EOptimizePropDiscr.v
@@ -715,22 +715,24 @@ Proof.
     * destruct with_guarded_fix.
       + move: i.
         rewrite !negb_or.
-        rewrite remove_match_on_box_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         rewrite !andb_true_r.
         rtoProp; intuition auto.
         destruct v => /= //.
         destruct v => /= //.
         destruct v => /= //.
+        destruct v => /= //.
       + move: i.
         rewrite !negb_or.
-        rewrite remove_match_on_box_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
   - depelim X; repeat constructor.
     eapply All2_over_undep in a. eapply All2_All2_Set. eapply All2_Set_All2 in ev. subst a0 a'; cbn in *.
     rewrite /test_array_model /= in H. rtoProp; intuition auto; solve_all. eapply e.
     cbn in H. rewrite /test_array_model /= in H. now move/andP: H => [].
+  - intros. econstructor; eauto. eapply IHev2. eapply eval_closed in ev1; tea.
   - destruct t => //.
     all:constructor; eauto. cbn [atom remove_match_on_box] in i |- *.
     rewrite -lookup_constructor_remove_match_on_box //. destruct args => //.
diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v
index c58d9e5d9..9780299a8 100644
--- a/erasure/theories/ERemoveParams.v
+++ b/erasure/theories/ERemoveParams.v
@@ -779,6 +779,14 @@ Proof.
   all:rewrite !isPrimApp_mkApps //.
 Qed.
 
+Lemma strip_isLazyApp Σ f :
+  isLazyApp f = isLazyApp (strip Σ f).
+Proof.
+  funelim (strip Σ f); cbn -[strip] => //.
+  all:rewrite map_InP_spec.
+  all:rewrite !isLazyApp_mkApps //.
+Qed.
+
 Lemma lookup_inductive_pars_is_prop_and_pars {Σ ind b pars} :
   inductive_isprop_and_pars Σ ind = Some (b, pars) ->
   lookup_inductive_pars Σ (inductive_mind ind) = Some pars.
@@ -1011,8 +1019,8 @@ Proof.
   - rewrite !strip_tApp //.
     eapply eval_app_cong; tea.
     move: H1. eapply contraNN.
-    rewrite -strip_isLambda -strip_isConstructApp -strip_isFixApp -strip_isBox -strip_isPrimApp //.
-    rewrite -strip_isFix //.
+    rewrite -strip_isLambda -strip_isConstructApp -strip_isFixApp -strip_isBox -strip_isPrimApp
+      -strip_isLazyApp // -strip_isFix //.
 
   - rewrite !strip_mkApps // /=.
     rewrite (lookup_constructor_lookup_inductive_pars H).
@@ -1030,6 +1038,8 @@ Proof.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. eapply All2_All2_Set. solve_all. now destruct b.
     now destruct a0.
 
+  - simp_strip. simp_strip in e0. econstructor; tea.
+
   - destruct t => //.
     all:constructor; eauto. simp strip.
     cbn [atom strip] in H |- *.
diff --git a/erasure/theories/EWcbvEval.v b/erasure/theories/EWcbvEval.v
index 7cd775a2a..6a6d78968 100644
--- a/erasure/theories/EWcbvEval.v
+++ b/erasure/theories/EWcbvEval.v
@@ -38,6 +38,7 @@ Definition atom `{wfl : WcbvFlags} Σ t :=
   | tBox
   | tCoFix _ _
   | tLambda _ _
+  | tLazy _
   | tFix _ _ => true
   | tConstruct ind c [] => negb with_constructor_as_block && isSome (lookup_constructor Σ ind c)
   | _ => false
@@ -258,7 +259,7 @@ Section Wcbv.
   | eval_app_cong f f' a a' :
       eval f f' ->
       ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f' || isConstructApp f'
-        || isPrimApp f')  ->
+        || isPrimApp f' || isLazyApp f')  ->
       eval a a' ->
       eval (tApp f a) (tApp f' a')
 
@@ -272,13 +273,12 @@ Section Wcbv.
     eval_primitive eval p p' ->
     eval (tPrim p) (tPrim p')
 
-  (*
-  | eval_lazy : eval (tLazy t) (tLazy t)
-  | eval_force t v v' : eval t (tLazy v) ->
+  | eval_force t v v' :
+    eval t (tLazy v) ->
     eval v v' ->
-    eval (tForce t) v' *)
+    eval (tForce t) v'
 
-  (** Atoms are values (includes abstractions, cofixpoints and constructors) *)
+  (** Atoms are values (includes abstractions, cofixpoints, constructors and lazy) *)
   | eval_atom t : atom Σ t -> eval t t.
 
   Hint Constructors eval : core.
@@ -615,7 +615,7 @@ Section eval_rect.
                                                  isBox f'
                                                  ||
                                                  isConstructApp f'
-                                                 || isPrimApp f'))
+                                                 || isPrimApp f' || isLazyApp f'))
                                            (e0 : eval Σ a a'),
                                            P a a' e0
                                            → P (tApp f16 a)
@@ -626,14 +626,17 @@ Section eval_rect.
 
     (forall p p' (ev : eval_primitive (eval Σ) p p'),
       eval_primitive_ind _ P _ _ ev ->
-      P (tPrim p) (tPrim p') (eval_prim _ _ _ ev))
+      P (tPrim p) (tPrim p') (eval_prim _ _ _ ev)) ->
+    (forall t t' v (ev1 : eval Σ t (tLazy t')) (ev2 : eval Σ t' v),
+      P _ _ ev1 -> P _ _ ev2 ->
+      P (tForce t) v (eval_force _ t t' v ev1 ev2))
 
-      → (∀ (t : term) (i : atom Σ t),
+    → (∀ (t : term) (i : atom Σ t),
           P t t (eval_atom Σ t i))
       → ∀ (t t0 : term) (e : eval Σ t t0),
           P t t0 e.
   Proof using Type.
-    intros ?????????????????????? H.
+    intros ??????????????????????? H.
     revert t t0 H.
     fix aux 3.
     move aux at top.
@@ -785,6 +788,7 @@ Section Wcbv.
         + destruct with_guarded_fix.
           now cbn in i1. now cbn in i1.
         + constructor.
+        + now destruct with_guarded_fix; cbn in i1.
         + cbn in i. destruct with_guarded_fix; cbn in i; rtoProp; intuition auto.
       * destruct b0 as (ind & c & mdecl & idecl & cdecl & args & [H1 H2 H3 H4]).
         rewrite -[tApp _ _](mkApps_app _ (firstn n l) [a']).
@@ -1058,7 +1062,7 @@ Section Wcbv.
       rewrite !mkApps_app /=.
       eapply eval_app_cong; tea.
       eapply IHargs => //.
-      rewrite isFixApp_mkApps // /= isConstructApp_mkApps // !negb_or isPrimApp_mkApps.
+      rewrite isFixApp_mkApps // /= isConstructApp_mkApps // !negb_or isPrimApp_mkApps isLazyApp_mkApps.
       rtoProp; intuition auto.
       apply nisLambda_mkApps => //.
       destruct with_guarded_fix => //; eapply nisFix_mkApps => //.
@@ -1304,15 +1308,15 @@ Section Wcbv.
         cbn in i. rtoProp; intuition auto.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite guarded in i. rtoProp; intuition auto.
-        rewrite isFixApp_mkApps in H3 => //.
+        rewrite isFixApp_mkApps in H4 => //.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite guarded in i. rtoProp; intuition auto.
-        rewrite isFixApp_mkApps in H3 => //.
+        rewrite isFixApp_mkApps in H4 => //.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite unguarded in i. now cbn in i.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rtoProp; intuition auto.
-        now rewrite isConstructApp_mkApps in H1.
+        now rewrite isConstructApp_mkApps in H2.
       + specialize (IHev1 _ ev'1); noconf IHev1.
         specialize (IHev2 _ ev'2); noconf IHev2.
         now assert (i0 = i) as -> by now apply uip.
@@ -1329,6 +1333,7 @@ Section Wcbv.
       induction ev in a, ev0 |- *; depelim ev0; eauto.
       destruct a.
       f_equal; eauto. specialize (e0 _ e). now noconf e0.
+    - depelim ev'; go.
     - depelim ev'; try go.
       2: now assert (i0 = i) as -> by now apply uip.
       exfalso. invs i. rewrite e in H0. destruct args; cbn in H0; invs H0.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
index dbaed8575..47d73387e 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
@@ -334,7 +334,7 @@ Lemma eval_preserve_mkApps_ind :
      P f11 f' ->
      (forall t u (ev' : eval Σ t u), eval_depth ev' <= eval_depth ev -> Q 0 t -> P t u) →
      ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f'
-      || isConstructApp f' || isPrimApp f') →
+      || isConstructApp f' || isPrimApp f' || isLazyApp f') →
      eval Σ a a' → P a a' →
      P' (tApp f11 a) (tApp f' a')) →
   (∀ ind i mdecl idecl cdecl args args',
@@ -349,6 +349,11 @@ Lemma eval_preserve_mkApps_ind :
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 
+  (forall t t' v, eval Σ t (tLazy t') -> eval Σ t' v ->
+    P t (tLazy t') ->
+    P t' v ->
+    P' (tForce t) v) ->
+
   (∀ t : term, atom Σ t → Q 0 t -> P' t t) ->
   ∀ (t t0 : term), Q 0 t -> eval Σ t t0 → P' t t0.
 Proof.
@@ -359,7 +364,7 @@ Proof.
   intros.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2.π2))).
-  set(foo := existT _ t (existT _ t0 (existT _ X17 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
+  set(foo := existT _ t (existT _ t0 (existT _ X18 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   change t with (projT1 foo).
   change t0 with (projT1 (projT2 foo)).
   revert foo.
@@ -369,8 +374,8 @@ Proof.
   forward p.
   2:{ apply p. apply measure_wf, lt_wf. }
   clear p.
-  rename X17 into qt. rename X14 into Xcappexp.
-  rename X15 into Qprim, X16 into Qatom.
+  rename X18 into qt. rename X14 into Xcappexp.
+  rename X15 into Qprim, X16 into Qforce, X17 into Qatom.
   clear t t0 qt H.
   intros (t & t0 & qt & ev).
   intros IH.
@@ -569,6 +574,15 @@ Proof.
       + depelim p0. destruct p.
         eapply and_assum. unshelve eapply IH; tea. cbn; lia.
         intros; split => //; eapply P'Q; tea.
+  - eapply qpres in qt; depelim qt => //.
+    assert (Q 0 (tLazy v)).
+    { eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    eapply qpres in X14. depelim X14 => //.
+    eapply Qforce; tea.
+    + eapply and_assum. eapply (IH _ _ q ev1); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
+    + eapply and_assum. eapply (IH _ _ q0 ev2); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
   - eapply Qatom; tea.
 Qed.
 
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
index 158684f81..955c25c0b 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
@@ -298,7 +298,7 @@ Lemma eval_preserve_mkApps_ind :
      P f11 f' ->
      (forall t u (ev' : eval Σ t u), eval_depth ev' <= eval_depth ev -> Q 0 t -> P t u) →
      ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f'
-      || isConstructApp f' || isPrimApp f') →
+      || isConstructApp f' || isPrimApp f' || isLazyApp f') →
      eval Σ a a' → P a a' →
      P' (tApp f11 a) (tApp f' a')) →
   (∀ ind i mdecl idecl cdecl args args',
@@ -313,6 +313,11 @@ Lemma eval_preserve_mkApps_ind :
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 
+  (forall t t' v, eval Σ t (tLazy t') -> eval Σ t' v ->
+    P t (tLazy t') ->
+    P t' v ->
+    P' (tForce t) v) ->
+
   (∀ t : term, atom Σ t → Q 0 t -> P' t t) ->
   ∀ (t t0 : term), Q 0 t -> eval Σ t t0 → P' t t0.
 Proof.
@@ -322,7 +327,7 @@ Proof.
   intros.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2.π2))).
-  set(foo := existT _ t (existT _ t0 (existT _ X16 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
+  set(foo := existT _ t (existT _ t0 (existT _ X17 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   change t with (projT1 foo).
   change t0 with (projT1 (projT2 foo)).
   revert foo.
@@ -332,8 +337,8 @@ Proof.
   forward p.
   2:{ apply p. apply measure_wf, lt_wf. }
   clear p.
-  rename X16 into qt. rename X13 into Xcappexp.
-  rename X14 into Qprim, X15 into Qatom.
+  rename X17 into qt. rename X13 into Xcappexp.
+  rename X14 into Qprim, X15 into Qforce, X16 into Qatom.
   clear t t0 qt H.
   intros (t & t0 & qt & ev).
   intros IH.
@@ -356,7 +361,7 @@ Proof.
   Ltac myt hyp anda P'Q := eapply hyp; tea; (apply and_assum; [ih|hp' P'Q]).
 
   destruct ev.
-  1-18:eapply qpres in qt as qt'; depelim qt' => //.
+  1-19:eapply qpres in qt as qt'; depelim qt' => //.
   all:try congruence.
   - eapply X; tea; (apply and_assum; [ih|hp' P'Q]).
   - assert (ql : Q 0 (tLambda na b)).
@@ -468,6 +473,15 @@ Proof.
       + depelim p0. destruct p.
         eapply and_assum. unshelve eapply IH; tea. cbn; lia.
         intros; split => //; eapply P'Q; tea.
+  - eapply qpres in qt; depelim qt => //.
+    assert (Q 0 (tLazy v)).
+    { eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    eapply qpres in X13. depelim X13 => //.
+    eapply Qforce; tea.
+    + eapply and_assum. eapply (IH _ _ q ev1); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
+    + eapply and_assum. eapply (IH _ _ q0 ev2); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
   - eapply Qatom; tea.
 Qed.
 
diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v
index f2058f16f..442a7ee29 100644
--- a/erasure/theories/EWcbvEvalEtaInd.v
+++ b/erasure/theories/EWcbvEvalEtaInd.v
@@ -308,7 +308,7 @@ Lemma eval_preserve_mkApps_ind :
      P f11 f' ->
      (forall t u (ev' : eval Σ t u), eval_depth ev' <= eval_depth ev -> Q 0 t -> isEtaExp Σ t -> P t u) →
      ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f' || isConstructApp f' ||
-      isPrimApp f') →
+      isPrimApp f' || isLazyApp f') →
      eval Σ a a' → P a a' →
      isEtaExp Σ (tApp f' a') ->
      P' (tApp f11 a) (tApp f' a')) →
@@ -326,11 +326,10 @@ Lemma eval_preserve_mkApps_ind :
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 
-  (* (forall t t', eval Σ t t' -> Q 0 t -> Q 0 t' -> P t t' ->
-    P' (tLazy t) (tLazy t')) ->
-
-  (forall t t', eval Σ t t' -> Q 0 t -> Q 0 t' -> P t t' ->
-    P' (tForce t) (tForce t')) -> *)
+  (forall t t' v, eval Σ t (tLazy t') -> eval Σ t' v ->
+    P t (tLazy t') ->
+    P t' v ->
+    P' (tForce t) v) ->
 
   (∀ t : term, atom Σ t → Q 0 t -> isEtaExp Σ t -> P' t t) ->
   ∀ (t t0 : term), Q 0 t -> isEtaExp Σ t -> eval Σ t t0 → P' t t0.
@@ -339,10 +338,10 @@ Proof.
   assert (qfixs: Qfixs Q) by tc.
   assert (qcofixs: Qcofixs Q) by tc.
   intros.
-  enough (P' t t0 × isEtaExp Σ t0). apply X17.
+  enough (P' t t0 × isEtaExp Σ t0). apply X18.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2.π2))).
-  set(foo := existT _ t (existT _ t0 (existT _ X16 H0)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
+  set(foo := existT _ t (existT _ t0 (existT _ X17 H0)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   move: H.
   change t with (projT1 foo).
   change t0 with (projT1 (projT2 foo)).
@@ -354,8 +353,9 @@ Proof.
   forward p.
   2:{ apply p. apply measure_wf, lt_wf. }
   clear p.
-  rename X16 into qt. rename X13 into Xcappexp.
-  rename X14 into Qprim. rename X15 into Qatom.
+  rename X17 into qt. rename X13 into Xcappexp.
+  rename X14 into Qprim. rename X15 into Qforce.
+  rename X16 into Qatom.
   clear t t0 qt H0.
   intros (t & t0 & qt & ev).
   intros IH.
@@ -381,7 +381,7 @@ Proof.
       eapply H; tea; (apply and_assum; [ih|hp' P'Q])
     end.
   destruct ev.
-  1-18:eapply qpres in qt as qt'; depelim qt' => //.
+  1-19:eapply qpres in qt as qt'; depelim qt' => //.
   - move/isEtaExp_tApp.
     destruct decompose_app as [hd args] eqn:da.
     destruct (construct_viewc hd) eqn:cv.
@@ -698,29 +698,44 @@ Proof.
       split; simp_eta. unshelve eapply Qprim. constructor; eauto. constructor.
       + apply All2_over_undep. cbn in IH.
         ELiftSubst.solve_all.
-        depelim H. destruct p as [[] ?].
+        depelim H0. destruct p as [[] a0].
         clear -ev IH a0 P'Q and_assum. cbn in a0. subst a; cbn in *.
         induction ev; constructor; eauto.
-        ** depelim a0. destruct p as [].
+        ** depelim a0. destruct p as [? []].
            eapply and_assum. unshelve eapply IH; tea. cbn. lia.
            intros []. split => //. split => //. eapply P'Q; tea.
         ** depelim a0. intuition eauto. eapply IHev; intros. 2:eauto.
            unshelve eapply IH; tea. cbn; lia.
-      + ELiftSubst.solve_all. depelim H; destruct p as [[] ?].
+      + ELiftSubst.solve_all. depelim H0. destruct p as [[? []] ?].
         eapply and_assum. unshelve eapply IH; tea. cbn; lia.
         intros []; split => //; split => //. eapply P'Q; tea.
       + ELiftSubst.solve_all. subst a a'; cbn in *.
-        depelim H; constructor; cbn in *; intuition eauto.
+        depelim H0; constructor; cbn in *; intuition eauto.
         unshelve eapply IH. 2:tea. all:eauto. cbn; lia.
         clear -ev IH b P'Q and_assum. cbn in b.
         induction ev; constructor; eauto.
-        ** depelim b. destruct p. unshelve eapply IH. 2:tea. all:eauto. cbn. lia.
+        ** depelim b. destruct p as [? []]. unshelve eapply IH. 2:tea. all:eauto. cbn. lia.
         ** depelim b. intuition eauto. eapply IHev; intros. 2:eauto.
            unshelve eapply IH; tea. cbn; lia.
- - intros ise. split => //. eapply Qatom; tea.
+  - simp_eta => ise.
+    eapply Qpres in qt. depelim qt => //.
+    assert (Q 0 (tLazy v)).
+    { eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    eapply qpres in X13. depelim X13 => //.
+    assert (isEtaExp Σ (tLazy v)) as etav.
+    { eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    simp_eta in etav.
+    split.
+    + unshelve eapply Qforce. 2:tea. auto.
+      eapply and_assum. eapply (IH _ _ q ev1); tea. now cbn; lia.
+      intros []. split => //. split => //. eapply P'Q; tea.
+      pose proof (IH _ _ q ev1). forward X13. cbn; lia. specialize (X13 ise) as [].
+      eapply and_assum. eapply (IH _ _ q0 ev2); tea. now cbn; lia.
+      now simp_eta in i1.
+    + eapply (IH _ _ q0 ev2) => //. now cbn; lia.
+  - intros ise. split => //. eapply Qatom; tea.
 Qed.
 
-
 From MetaCoq.Erasure Require Import ELiftSubst.
 Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ :
   cstr_as_blocks = false ->
diff --git a/erasure/theories/EWcbvEvalInd.v b/erasure/theories/EWcbvEvalInd.v
index 05328f1ef..8e0f365b2 100644
--- a/erasure/theories/EWcbvEvalInd.v
+++ b/erasure/theories/EWcbvEvalInd.v
@@ -238,7 +238,7 @@ Section eval_mkApps_rect.
                  then isFixApp f'
                  else isFix f') ||
                 isBox f' ||
-                isConstructApp f' || isPrimApp f'))
+                isConstructApp f' || isPrimApp f' || isLazyApp f'))
           (e0 : eval Σ a a'),
           P a a'
           → P (tApp f15 a)
@@ -246,12 +246,15 @@ Section eval_mkApps_rect.
 
    (forall p p' (ev : eval_primitive (eval Σ) p p'),
       eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
-      P (tPrim p) (tPrim p'))
+      P (tPrim p) (tPrim p')) ->
 
+   (forall t t' v (ev1 : eval Σ t (tLazy t')) (ev2 : eval Σ t' v),
+      P t (tLazy t') -> P t' v ->
+      P (tForce t) v)
     → (∀ t : term, atom Σ t → P t t)
     → ∀ t t0 : term, eval Σ t t0 → P t t0.
 Proof using Type.
-  intros ?????????????????????? H.
+  intros ??????????????????????? H.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & eval Σ t t0 }}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2))).
   set(foo := existT _ t (existT _ t0 H) :  { t : _ & { t0 : _ & eval Σ t t0 }}).
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index 02816f1d3..a3ac397de 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -36,7 +36,8 @@ Inductive value : Set :=
 | vClos (na : ident) (b : term) (env : list (ident * value))
 | vConstruct (ind : inductive) (c : nat) (args : list (value))
 | vRecClos (b : list (ident * term)) (idx : nat) (env : list (ident * value))
-| vPrim (p : EPrimitive.prim_val value).
+| vPrim (p : EPrimitive.prim_val value)
+| vLazy (p : term) (env : list (ident * value)).
 
 Definition environment := list (ident * value).
 Definition add : ident -> value -> environment -> environment := fun (x : ident) (v : value) env =>
@@ -148,7 +149,14 @@ Section Wcbv.
 
   | eval_prim p p' :
     eval_primitive (eval Γ) p p' ->
-    eval Γ (tPrim p) (vPrim p').
+    eval Γ (tPrim p) (vPrim p')
+
+  | eval_lazy t : eval Γ (tLazy t) (vLazy t Γ)
+  | eval_force Γ' t t' v :
+    eval Γ t (vLazy t' Γ') ->
+    eval Γ' t' v ->
+    eval Γ (tForce t) v
+  .
 
   Program Definition eval_ind :=
     λ (P : ∀ (Γ : environment) (t : term) (v : value), eval Γ t v → Type) (f : ∀ (Γ : environment) (na : string) (v : value) (e : lookup Γ na = Some v),
@@ -247,7 +255,11 @@ Section Wcbv.
           P Γ (tConstruct ind c []) (vConstruct ind c []) (eval_construct_block_empty Γ ind c mdecl idecl cdecl e))
       (f10 : ∀ (Γ : environment) (p : prim_val term) (p' : prim_val value) (ev : eval_primitive (eval Γ) p p')
         (evih : eval_primitive_ind (eval Γ) (P Γ) _ _ ev),
-        P Γ (tPrim p) (vPrim p') (eval_prim _ _ _ ev)),
+        P Γ (tPrim p) (vPrim p') (eval_prim _ _ _ ev))
+      (f11 :∀ (Γ : environment) t, P Γ (tLazy t) (vLazy t Γ) (eval_lazy _ _))
+      (f12 : ∀ Γ Γ' t t' v (ev0 : eval Γ t (vLazy t' Γ')) (ev1 : eval Γ' t' v),
+        P _ _ _ ev0 -> P _ _ _ ev1 ->
+        P _ _ _ (eval_force _ _ _ _ _ ev0 ev1)),
       fix F (Γ : environment) (t : term) (v : value) (e : eval Γ t v) {struct e} : P Γ t v e :=
       match e as e0 in (eval _ t0 v0) return (P Γ t0 v0 e0) with
       | @eval_var _ na v0 e0 => f Γ na v0 e0
@@ -263,6 +275,8 @@ Section Wcbv.
       | @eval_construct_block _ ind c mdecl idecl cdecl args args' e0 l a => f8 Γ ind c mdecl idecl cdecl args args' e0 l a (map_All2_dep _ (F Γ) a)
       | @eval_construct_block_empty _ ind c mdecl idecl cdecl e0 => f9 Γ ind c mdecl idecl cdecl e0
       | @eval_prim _ p p' ev => f10 Γ p p' ev (map_eval_primitive (P := P Γ) (F Γ) ev)
+      | @eval_lazy _ t => f11 Γ t
+      | @eval_force _ Γ' t t' v ev ev' => f12 _ _ _ _ _ ev ev' (F Γ _ _ ev) (F Γ' _ _ ev')
       end.
 
 End Wcbv.
@@ -307,6 +321,7 @@ with represents_value : value -> term -> Set :=
 | represents_value_tFix vfix i E mfix :
   All2_Set (fun v d => isLambda (snd v) × (List.rev (map fst vfix) ;;; E ⊩ snd v ~ d.(dbody))) vfix mfix -> represents_value (vRecClos vfix i E) (tFix mfix i)
 | represents_value_tPrim p p' : onPrims represents_value p p' -> represents_value (vPrim p) (tPrim p')
+| represents_value_tLazy E t t' : [] ;;; E ⊩ t ~ t' -> represents_value (vLazy t E) (tLazy t')
 where "Γ ;;; E ⊩ s ~ t" := (represents Γ E s t).
 Derive Signature for represents represents_value.
 
@@ -413,7 +428,9 @@ Program Definition represents_ind :=
          P0 (vRecClos vfix i E) (tFix mfix i)
            (represents_value_tFix vfix i E mfix a))
      (f13 : forall p p' (o : onPrims represents_value p p'), onPrims_dep _ P0 _ _ o ->
-        P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o)),
+        P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o))
+    (f14 : forall E t t' (r : represents [] E t t'), P [] E t t' r ->
+      P0 (vLazy t E) (tLazy t') (represents_value_tLazy E t t' r)),
     fix F
       (l : list ident) (e : environment) (t t0 : term)
       (r : l;;; e ⊩ t ~ t0) {struct r} : P l e t t0 r :=
@@ -450,6 +467,7 @@ Program Definition represents_ind :=
           | represents_value_tConstruct vs ts ind c a => f11 vs ts ind c a _
           | represents_value_tFix vfix i E mfix a => f12 vfix i E mfix a _
           | represents_value_tPrim p p' r => f13 p p' r (map_onPrims F0 r)
+          | represents_value_tLazy E t t' r => f14 E t t' r (F [] E t t' r)
           end
             for
             F).
@@ -578,7 +596,9 @@ Program Definition represents_value_ind :=
          P0 (vRecClos vfix i E) (tFix mfix i)
            (represents_value_tFix vfix i E mfix a))
     (f13 : forall p p' (o : onPrims represents_value p p'), onPrims_dep _ P0 _ _ o ->
-           P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o)),
+           P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o))
+    (f14 : forall E t t' (r : represents [] E t t'), P [] E t t' r ->
+        P0 (vLazy t E) (tLazy t') (represents_value_tLazy E t t' r)),
 
     fix F
       (l : list ident) (e : environment) (t t0 : term)
@@ -617,6 +637,7 @@ Program Definition represents_value_ind :=
           | represents_value_tConstruct vs ts ind c a => f11 vs ts ind c a _
           | represents_value_tFix vfix i E mfix a => f12 vfix i E mfix a _
           | represents_value_tPrim p p' r => f13 p p' r (map_onPrims F0 r)
+          | represents_value_tLazy E t t' r => f14 E t t' r (F [] E t t' r)
           end
             for
             F0).
@@ -746,9 +767,10 @@ Definition rep_ind :=
            (represents_value_tFix vfix i E mfix a))
       (f13 : forall p p' (o : onPrims represents_value p p'), onPrims_dep _ P0 _ _ o ->
            P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o))
+      f14
            ,
-    (represents_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13,
-      represents_value_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13)).
+    (represents_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13 f14,
+      represents_value_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13 f14)).
 
 Local Notation "'⊩' v ~ s" := (represents_value v s) (at level 50).
 Local Hint Constructors represents : core.
@@ -1226,7 +1248,7 @@ Lemma unfolds_bound :
   (forall Γ E s t, Γ ;;; E ⊩ s ~ t -> closedn #|Γ| t) ×
     (forall v s, ⊩ v ~ s -> closedn 0 s).
 Proof.
-  refine (rep_ind _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); intros; cbn; rtoProp; eauto.
+  refine (rep_ind _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); intros; cbn; rtoProp; eauto.
   - eapply Nat.ltb_lt, nth_error_Some. congruence.
   - eapply closed_upwards; eauto. lia.
   - solve_all. induction a; cbn in *; econstructor; firstorder.
@@ -1515,7 +1537,8 @@ Inductive wf : value -> Type :=
   All (fun t => sunny (map fst vfix ++ map fst E) (snd t)) vfix ->
   All (fun v => wf (snd v)) E ->
   wf (vRecClos vfix idx E)
-| wf_vPrim p : primProp wf p -> wf (vPrim p).
+| wf_vPrim p : primProp wf p -> wf (vPrim p)
+| wf_vLazy E t : sunny (map fst E) t -> All (fun v => wf (snd v)) E -> wf (vLazy t E).
 
 Lemma declared_constant_Forall P Σ c decl :
   Forall (P ∘ snd) Σ ->
@@ -1609,6 +1632,8 @@ Proof.
   - rtoProp; solve_all.
 Qed.
 
+Derive NoConfusion for value.
+
 Lemma eval_wf Σ E s v :
   Forall (fun d => match d.2 with ConstantDecl (Build_constant_body (Some d)) => sunny [] d | _ => true end) Σ ->
   All (fun x => wf (snd x)) E ->
@@ -1723,6 +1748,8 @@ Proof.
   - cbn. econstructor. econstructor.
   - econstructor. solve_all. depelim evih; depelim Hsunny; try subst a0 a'; cbn; constructor; cbn in *; intuition solve_all.
     eapply All2_over_undep in a. solve_all.
+  - econstructor; eauto.
+  - eapply X in HE; eauto. depelim HE. eapply X0; eauto.
 Qed.
 
 Lemma eval_construct_All2 Σ E ind c args vs mdecl idecl cdecl :
@@ -2154,6 +2181,12 @@ Proof.
         { clear -Hvs; induction Hvs; constructor; intuition eauto. }
       + constructor; eauto. eapply All2_All2_Set.
         { clear -Hvs; induction Hvs; constructor; intuition eauto. }
+  - invs Hrep; cbn in *; rtoProp. depelim H2.
+    apply s0 in H5 as [v' [reprev t1v]]; eauto.
+    depelim reprev.
+    eapply eval_wf in HΣ; tea. depelim HΣ.
+    eapply s1 in r as [v2 [reprv2 evv2]]; eauto.
+    exists v2. split => //. econstructor; eauto.
   - invs Hrep; cbn in *; try congruence; rtoProp.
     + econstructor. split; eauto. econstructor. eauto.
     + econstructor. split; eauto. econstructor.
@@ -2170,8 +2203,8 @@ Proof.
       intros.
       cbn in *. destruct H5 as (([? []] & ?) & ?).
       rewrite app_nil_r in r. all: eauto.
-
-      Unshelve. all: repeat econstructor.
+    + exists (vLazy t1 E). now split; econstructor.
+  Unshelve. all: repeat econstructor.
 Qed.
 
 Lemma concat_sing {X} l :
diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
index 4a12486ef..4dcabe930 100644
--- a/erasure/theories/ErasureCorrectness.v
+++ b/erasure/theories/ErasureCorrectness.v
@@ -40,6 +40,14 @@ Notation "Σ ⊢ s ⇓ t" := (EWcbvEval.eval Σ s t) (at level 50, s, t at next
 
 Import ssrbool.
 
+Lemma erases_lazy Σ Γ t t' : Σ ;;; Γ |- t ⇝ℇ t' -> EAstUtils.isLazyApp t' -> False.
+Proof.
+  rewrite /EAstUtils.isLazyApp /EAstUtils.head /EAstUtils.decompose_app.
+  generalize (@nil EAst.term) as l; intros l.
+  induction 1 in l |- *; cbn => //=.
+  eapply IHerases1.
+Qed.
+
 Lemma erases_correct (wfl := default_wcbv_flags) Σ t t' v Σ' :
   wf_ext Σ ->
   welltyped Σ [] t ->
@@ -1150,6 +1158,10 @@ Proof.
         -- rewrite !negb_or in i. rtoProp; intuition auto.
            eapply is_PrimApp_erases in H8; tea.
            now move/negbTE: H8.
+        -- rewrite !negb_or in i.
+           rtoProp; intuition auto.
+           apply/negbTE. apply PCUICNormal.negb_is_true => isl.
+           eapply erases_lazy in H1; tea.
     + exists EAst.tBox. split. 2: now constructor; econstructor.
       econstructor.
       eapply inversion_App in Hty as [na [A [B [Hf [Ha _]]]]]; auto.
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index 92bc3b69e..a8f685dfc 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -2017,6 +2017,8 @@ Proof.
   - depelim X; auto.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. solve_all. subst a0 a'; cbn in *.
     depelim exp_t; constructor; cbn in *; intuition eauto. solve_all.
+  - eapply IHev1 in exp_t. eapply IHev2 in exp_t.
+    eapply is_expanded_aux_upwards; tea. lia.
 Qed.
 
 Lemma valid_case_masks_lift ind c brs n k :
@@ -2823,6 +2825,7 @@ Proof with auto with dearg.
   - depelim X; auto.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. subst a0 a'; cbn -[test_prim] in *.
     solve_all. depelim H0; constructor; cbn; intuition eauto. solve_all.
+  - eapply IHev2. eapply eval_closed in ev1; tea. eapply IHev1; eauto.
 Qed.
 
 Lemma declared_constant_dearg Σ k cst :
@@ -3452,22 +3455,22 @@ Section dearg.
           cbn in *; propify.
           rewrite dearg_single_masked by (now rewrite map_length).
           rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps;cbn in *.
-          rewrite isPrimApp_mkApps.
-          destruct with_guarded_fix;cbn;auto.
+          rewrite isPrimApp_mkApps, isLazyApp_mkApps in *.
+          destruct with_guarded_fix;cbn;intuition auto.
           now rewrite EOptimizePropDiscr.isFix_mkApps;cbn.
         * rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps in *;cbn in *.
           propify.
           destruct with_guarded_fix;cbn in *; intuition.
         * unfold dearg_case.
           destruct with_guarded_fix;cbn.
-          now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps;cbn.
-          now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps;cbn.
+          now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
+          now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
         * unfold dearg_proj.
           unfold dearg_case.
           destruct with_guarded_fix;cbn.
-          ** now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps;cbn.
-          ** now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps;cbn.
-        * rewrite !isLambda_mkApps, !isFixApp_mkApps, !EOptimizePropDiscr.isFix_mkApps, !isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps in *
+          ** now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
+          ** now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
+        * rewrite !isLambda_mkApps, !isFixApp_mkApps, !EOptimizePropDiscr.isFix_mkApps, !isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps, isLazyApp_mkApps in *
             by now destruct hd.
           rewrite map_length.
           destruct with_guarded_fix;cbn;auto;
@@ -4971,6 +4974,9 @@ Proof.
       unshelve eapply IHb0; tea. cbn in deriv_len. lia.
       cbn in *; unfold test_array_model in *; subst a a'; cbn in *.
       unshelve eapply IH; tea; rtoProp; intuition eauto. lia.
+    + facts. econstructor. specialize (IH _ _ clos_t valid_t exp_t ev1).
+      cbn in IH. apply IH. lia.
+      now forward (IH v _ H2 H4 H6 ev2).
     + destruct t; cbn in *; try destruct y; try congruence; now constructor.
 Qed.
 End dearg_correct.
diff --git a/erasure/theories/Typed/WcbvEvalAux.v b/erasure/theories/Typed/WcbvEvalAux.v
index e24e82804..11b2d6413 100644
--- a/erasure/theories/Typed/WcbvEvalAux.v
+++ b/erasure/theories/Typed/WcbvEvalAux.v
@@ -307,6 +307,7 @@ Fixpoint deriv_length {Σ t v} (ev : Σ e⊢ t ⇓ v) : nat :=
       S (deriv_length ev1 + deriv_length ev2 + deriv_length ev3)
   | eval_construct_block _ _ _ _ _ args _ _ _ _ _ => S #|args|
   | eval_prim _ _ ev => S (eval_prim_length (@deriv_length _) ev)
+  | eval_force _ _ _ ev ev' => S (deriv_length ev + deriv_length ev')
   end.
 
 Lemma deriv_length_min {Σ t v} (ev : Σ e⊢ t ⇓ v) :