diff --git a/theories/coneris/adequacy.v b/theories/coneris/adequacy.v
index d2d91710..d46d46fc 100644
--- a/theories/coneris/adequacy.v
+++ b/theories/coneris/adequacy.v
@@ -21,33 +21,32 @@ Section adequacy.
   Proof. iSplit; iIntros; simpl; iApply fupd_idemp; iFrame. Qed.
   
   Lemma pgl_dbind' `{Countable A, Countable A'}
-    (f : A → distr A') (μ : distr A) (R : A → Prop) (T : A' → Prop) ε ε' n :
-    ⌜ 0 <= ε ⌝ -∗
+    (f : A → distr A') (μ : distr A) (T : A' → Prop) ε' n :
     ⌜ 0 <= ε' ⌝ -∗
-    ⌜pgl μ R ε⌝ -∗
-    (∀ a , ⌜R a⌝ ={∅}=∗ |={∅}▷=>^(n) ⌜pgl (f a) T ε'⌝) -∗
-    |={∅}=> |={∅}▷=>^(n) ⌜pgl (dbind f μ) T (ε + ε')⌝ : iProp Σ.
+    (∀ a , |={∅}=>|={∅}▷=>^(n) ⌜pgl (f a) T ε'⌝) -∗
+    |={∅}=> |={∅}▷=>^(n) ⌜pgl (dbind f μ) T (ε')⌝ : iProp Σ.
   Proof.
-    iIntros (???) "H".
-    iApply (step_fupdN_mono _ _ _ (⌜(∀ a b, R a → pgl (f a) T ε')⌝)).
-    { iIntros (?). iPureIntro. eapply pgl_dbind; eauto. }
-    iIntros (???) "/=".
-    iApply ("H" with "[//]"). 
+    iIntros (?) "H".
+    iApply (step_fupdN_mono _ _ _ (⌜(∀ a, pgl (f a) T ε')⌝)).
+    { iIntros (?). iPureIntro.
+      rewrite <-Rplus_0_l. eapply pgl_dbind; try done.
+      by apply pgl_trivial. }
+    iIntros (?) "/=".
+    iApply "H". 
   Qed.
   
   Lemma pgl_dbind_adv' `{Countable A, Countable A'}
-    (f : A → distr A') (μ : distr A) (R : A → Prop) (T : A' → Prop) ε ε' n :
-    ⌜ 0 <= ε ⌝ -∗
+    (f : A → distr A') (μ : distr A) (T : A' → Prop) ε' n :
     ⌜ exists r, forall a, 0 <= ε' a <= r ⌝ -∗
-    ⌜pgl μ R ε⌝ -∗
-    (∀ a , ⌜R a⌝ ={∅}=∗ |={∅}▷=>^(n) ⌜pgl (f a) T (ε' a)⌝) -∗
-    |={∅}=> |={∅}▷=>^(n) ⌜pgl (dbind f μ) T (ε + Expval μ ε')⌝ : iProp Σ.
+    (∀ a , |={∅}=> |={∅}▷=>^(n) ⌜pgl (f a) T (ε' a)⌝) -∗
+    |={∅}=> |={∅}▷=>^(n) ⌜pgl (dbind f μ) T ( Expval μ ε')⌝ : iProp Σ.
   Proof.
-    iIntros (???) "H".
-    iApply (step_fupdN_mono _ _ _ (⌜(∀ a b, R a → pgl (f a) T (ε' a))⌝)).
-    { iIntros (?). iPureIntro. eapply pgl_dbind_adv; eauto. }
-    iIntros (???) "/=".
-    iApply ("H" with "[//]").
+    iIntros (?) "H".
+    iApply (step_fupdN_mono _ _ _ (⌜(∀ a, pgl (f a) T (ε' a))⌝)).
+    { iIntros (?). iPureIntro. rewrite <-Rplus_0_l. eapply pgl_dbind_adv; try done.
+      by apply pgl_trivial.
+    }
+    by iIntros (?) "/=".
   Qed.
 
   Lemma wp_adequacy_val_fupd `{Countable sch_int_state}  (ζ : sch_int_state) e es (sch: scheduler con_prob_lang_mdp sch_int_state) n v σ ε φ `{!TapeOblivious sch_int_state sch}:
@@ -63,7 +62,7 @@ Section adequacy.
     iRevert (σ ε) "H".
     iApply state_step_coupl_ind.
     iModIntro.
-    iIntros (??) "[%|[>(_&_&%)|[H|(%R&%μ&%&%&%Herasable&%&%Hineq&%Hpgl&H)]]]".
+    iIntros (??) "[%|[>(_&_&%)|[H|(%μ&%&%Herasable&%&%Hineq&H)]]]".
     - iPureIntro. by apply pgl_1.
     - iApply fupd_mask_intro; first done.
       iIntros "_".
@@ -85,11 +84,11 @@ Section adequacy.
       { iPureIntro.
         intros H'.
         eapply pgl_mon_grading; first apply Hineq.
-        eapply pgl_dbind_adv; [auto| |exact H'|exact].
-        naive_solver.
+        rewrite <-Rplus_0_l.
+        eapply pgl_dbind_adv; [| |exact H'|by apply pgl_trivial]; naive_solver.
       }
       iIntros (??).
-      by iMod ("H" with "[//]") as "[? _]".
+      by iMod ("H" $! _) as "[? _]".
   Qed.
 
   Lemma state_step_coupl_erasure `{Countable sch_int_state} (ζ : sch_int_state) es σ ε Z n (sch: scheduler con_prob_lang_mdp sch_int_state) φ `{H0 : !TapeOblivious sch_int_state sch}:
@@ -101,7 +100,7 @@ Section adequacy.
   Proof.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%Herasable&%&%&%&H)]]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%μ&%&%Herasable&%&%Hineq&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       by apply pgl_1.
@@ -117,13 +116,13 @@ Section adequacy.
       iApply ("H" with "[$]").
     - apply sch_erasable_sch_erasable_val in Herasable.
       rewrite -Herasable.
-      iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
+      iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_)⌝)%I).
       { iPureIntro.
-        intros. eapply pgl_mon_grading; exact.
+        intros. eapply pgl_mon_grading; first (simpl; apply Hineq). exact.
       }
-      iApply (pgl_dbind_adv' with "[][][][-]"); [done|naive_solver|done|].
-      iIntros (??).
-      iMod ("H" with "[//]") as "[H _]".
+      iApply (pgl_dbind_adv' with "[][-]"); first (iPureIntro; naive_solver).
+      iIntros (?).
+      iMod ("H"$!_) as "[H _]".
       simpl.
       iApply ("H" with "[$]").
   Qed.
@@ -141,7 +140,7 @@ Section adequacy.
     intros ???.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%&%&%&%&H)]]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%μ&%&%Herasable&%&%Hineq&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       by apply pgl_1.
@@ -156,13 +155,13 @@ Section adequacy.
         [pose proof cond_nonneg ε; simpl in *; lra|done|simpl].
       iApply ("H" with "[$]").
     - unshelve erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim_sch_erasable _ _ _ _ _ _ _ μ _ _ _ _)); [done..|].
-      iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
+      iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ _⌝)%I).
       { iPureIntro.
-        intros. eapply pgl_mon_grading; exact.
+        intros. eapply pgl_mon_grading; first (simpl; apply Hineq). exact.
       }
-      iApply (pgl_dbind_adv'); [done|naive_solver|done|].
-      iIntros (??).
-      iMod ("H" with "[//]") as "[H _]".
+      iApply (pgl_dbind_adv'); first (iPureIntro; naive_solver).
+      iIntros (?).
+      iMod ("H" $! _) as "[H _]".
       simpl.
       iApply ("H" with "[$]").
   Qed.
@@ -192,15 +191,12 @@ Section adequacy.
         repeat iModIntro.
         by iApply step_fupdN_intro.
       + rewrite {1}/sch_step. rewrite <-dbind_assoc.
-        replace (ε) with (0+ε)%NNR; last (apply nnreal_ext;simpl; lra).
+        (* replace (ε) with (0+ε)%NNR; last (apply nnreal_ext;simpl; lra). *)
         iApply fupd_mask_intro; first done.
         iIntros "Hclose".
         rewrite -fupd_idemp.
-        iApply (pgl_dbind' _ _ _ _ _ _ (S _)); [done|
-                             iPureIntro; apply cond_nonneg|
-                             iPureIntro;apply pgl_trivial;simpl;lra|
-                             ..].
-        iIntros ([sch_σ sch_a] _).
+        iApply (pgl_dbind' _ _ _ _ (S _)); first done.
+        iIntros ([sch_σ sch_a]).
         iMod "Hclose" as "_".
         simpl. rewrite Heq.
         destruct ((e::es)!!sch_a) as [chosen_e|] eqn:Hlookup; rewrite Hlookup; last first.
@@ -210,8 +206,6 @@ Section adequacy.
           iIntros "Hclose".
           do 2 iModIntro. iMod "Hclose" as "_".
           iApply "IH". iFrame.
-          iApply ec_supply_eq; last done.
-          simpl. lra.
         }
         case_match eqn:Hcheckval.
         { (* step a thread thats a value *)
@@ -220,8 +214,6 @@ Section adequacy.
           iIntros "Hclose".
           do 2 iModIntro. iMod "Hclose" as "_".
           iApply "IH". iFrame.
-          iApply ec_supply_eq; last done.
-          simpl. lra.
         }
         rewrite dmap_comp/dmap-dbind_assoc.
         erewrite (distr_ext _ _); last first.
@@ -234,17 +226,17 @@ Section adequacy.
         *  (* step main thread *)
           rewrite pgl_wp_unfold /pgl_wp_pre. iSimpl in "Hwp". rewrite Heq.
           iMod ("Hwp" with "[$]") as "Hlift".
-          replace (0+ε)%NNR with ε; [|apply nnreal_ext; simpl; lra].
+          (* replace (0+ε)%NNR with ε; [|apply nnreal_ext; simpl; lra]. *)
           iApply (state_step_coupl_erasure' with "[$Hlift]"); [done..|].
-          iIntros (σ2 ε2) "(%&%&%&%&%&%&%&H)".
-          iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
+          iIntros (σ2 ε2) "(%&%&%&%Hineq&H)".
+          iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ _⌝)%I).
           { iPureIntro.
-            intros. eapply pgl_mon_grading; exact.
+            intros. eapply pgl_mon_grading; first (simpl; apply Hineq). exact.
           }
           replace (chosen_e) with e; last by (simpl in Hlookup; simplify_eq).
-          iApply (pgl_dbind_adv' with "[][][][-]"); [done|naive_solver|done|].
-          iIntros ([[??]?]?).
-          iMod ("H" with "[//]") as "H".
+          iApply (pgl_dbind_adv' with "[][-]"); first (iPureIntro; naive_solver).
+          iIntros ([[??]?]).
+          iMod ("H" $! _ _ _ ) as "H".
           simpl.
           do 3 iModIntro.
           iApply (state_step_coupl_erasure with "[$][-]").
@@ -258,20 +250,20 @@ Section adequacy.
           iSimpl in "Hwp'".
           rewrite Hcheckval.
           iMod ("Hwp'" with "[$]") as "Hlift".
-          replace (0+ε)%NNR with ε; [|apply nnreal_ext; simpl; lra].
+          (* replace (0+ε)%NNR with ε; [|apply nnreal_ext; simpl; lra]. *)
           iApply (state_step_coupl_erasure' _ e _ chosen_e with "[$]"); [|done..|].
           { simpl.
             rewrite lookup_app_r//.
             by replace (_-_)%nat with 0%nat by lia.
           }
-          iIntros (σ2 ε2) "(%&%&%&%&%&%&%&H)".
-          iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
+          iIntros (σ2 ε2) "(%&%&%&%Hineq&H)".
+          iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ _⌝)%I).
           { iPureIntro.
-            intros. eapply pgl_mon_grading; exact.
+            intros. eapply pgl_mon_grading; first (simpl; apply Hineq). exact.
           }
-          iApply (pgl_dbind_adv' with "[][][][-]"); [done|naive_solver|done|].
-          iIntros ([[??]?]?).
-          iMod ("H" with "[//]") as "H".
+          iApply (pgl_dbind_adv' with "[][-]"); first (iPureIntro; naive_solver). 
+          iIntros ([[??]?]).
+          iMod ("H" $! _ _ _) as "H".
           simpl.
           do 3 iModIntro.
           iApply (state_step_coupl_erasure with "[$][-]").
@@ -488,7 +480,7 @@ Section safety.
   Proof.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%Herasable&%&%&%&H)]]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%μ&%&%Herasable&%&%&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       trans 0; try lra.
@@ -521,17 +513,17 @@ Section safety.
         - f_equal. by rewrite H4.
         - by rewrite !dmap_mass in H5.
       }
-      iApply (step_fupdN_mono _ _ _ (⌜SeriesC (μ ≫= λ σ', sch_pexec sch n (ζ, (es, σ'))) >= 1 - (ε1 + Expval μ ε2)⌝)).
+      iApply (step_fupdN_mono _ _ _ (⌜SeriesC (μ ≫= λ σ', sch_pexec sch n (ζ, (es, σ'))) >= 1 - (0 + Expval μ ε2)⌝)).
       { iPureIntro. intros. etrans; first exact.
         apply Rle_ge.
         apply Ropp_le_cancel.
-        rewrite !Ropp_minus_distr. by apply Rplus_le_compat_r. 
+        rewrite !Ropp_minus_distr. rewrite Rplus_0_l. by apply Rplus_le_compat_r. 
       }
-      iApply (safety_dbind_adv' _ _ _ (_)); [| |done|].
+      iApply (safety_dbind_adv' _ _ _ (_)); [| |iPureIntro; by apply pgl_trivial|].
       { iPureIntro. eapply sch_erasable_mass; last first; done. }
       { iPureIntro. naive_solver. }
       iIntros (a HR).
-      iMod ("H" with "[//]") as "[H _]".
+      iMod ("H" $! _) as "[H _]".
       by iMod ("H" with "[$]").
   Qed. 
 
@@ -548,7 +540,7 @@ Section safety.
     intros ???.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%Herasable&%&%&%&H)]]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%μ&%&%Herasable&%&%&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       trans 0; try lra.
@@ -585,17 +577,17 @@ Section safety.
           apply Rcoupl_eq_elim in K'. by rewrite K'.
         - by rewrite !dmap_mass in K.
       }
-      iApply (step_fupdN_mono _ _ _ (⌜SeriesC (μ ≫= (λ σ', prim_step e' σ' ≫= λ '(e3, σ3, efs), sch_pexec sch n (ζ, (<[num:=e3]> (e :: es) ++ efs, σ3)))) >= 1 - (ε1 + Expval μ ε2)⌝)).
+      iApply (step_fupdN_mono _ _ _ (⌜SeriesC (μ ≫= (λ σ', prim_step e' σ' ≫= λ '(e3, σ3, efs), sch_pexec sch n (ζ, (<[num:=e3]> (e :: es) ++ efs, σ3)))) >= 1 - (0 + Expval μ ε2)⌝)).
       { iPureIntro. intros. etrans; first exact.
         apply Rle_ge.
         apply Ropp_le_cancel.
-        rewrite !Ropp_minus_distr. by apply Rplus_le_compat_r.
+        rewrite !Ropp_minus_distr. rewrite Rplus_0_l. by apply Rplus_le_compat_r.
       }
-      iApply (safety_dbind_adv' _ _ _ (_)); [| |done|].
+      iApply (safety_dbind_adv' _ _ _ (_)); [| |iPureIntro; by apply pgl_trivial|].
       { iPureIntro. eapply sch_erasable_mass; last first; done. }
       { iPureIntro. naive_solver. }
       iIntros (a HR).
-      iMod ("H" with "[//]") as "[H _]".
+      iMod ("H" $! _) as "[H _]".
       by iMod ("H" with "[$]").
   Qed.
   
@@ -654,24 +646,24 @@ Section safety.
         iApply (state_step_coupl_erasure_safety'  with "[$Hwp]"); try done.
         iIntros (σ2 ε2). simpl. rewrite Hval.
         rewrite /prog_coupl.
-        iIntros "(%R&%εa & %εb & %Hred &%Hbound & %Hineq & %Hpgl & Hlift)".
+        iIntros "( %εb & %Hred &%Hbound & %Hineq &  Hlift)".
         assert (e = chosen_e) as ?; last simplify_eq.
         { simpl in Hlookup. by simplify_eq. }
         iApply (step_fupdN_mono _ _ _ (⌜SeriesC
            (prim_step chosen_e σ2 ≫= λ '(e3, σ3, efs), sch_pexec sch n (ζ', (e3 :: es ++ efs, σ3))) >=
-                                         1 - (εa + Expval (prim_step chosen_e σ2) εb)⌝)).
+                                         1 - (0 + Expval (prim_step chosen_e σ2) εb)⌝)).
         { iPureIntro. simpl in *.
           intros. etrans; first exact.
           apply Rle_ge.
           apply Ropp_le_cancel.
-          rewrite !Ropp_minus_distr. by apply Rplus_le_compat_r. 
+          rewrite !Ropp_minus_distr. rewrite Rplus_0_l. by apply Rplus_le_compat_r. 
         }
         iApply (safety_dbind_adv' _ _ _ _ (S n) with "[][][]").
         * iPureIntro. eapply mixin_prim_step_mass; [apply con_language_mixin|done].
         * iPureIntro. naive_solver.
-        * done.
-        * iIntros (((e' & σ') & efs) HR).
-          iMod ("Hlift" with "[//]").
+        * iPureIntro; by apply pgl_trivial.
+        * iIntros (((e' & σ') & efs) _).
+          iMod ("Hlift"$! _ _ _).
           simpl.
           do 3 iModIntro.
           iApply (state_step_coupl_erasure_safety with "[$]").
@@ -688,22 +680,23 @@ Section safety.
         iApply (state_step_coupl_erasure_safety'  with "[$]"); try done.
         { simpl. by apply list_lookup_middle. }
         iIntros (σ2 ε2). simpl. rewrite /prog_coupl. 
-        iIntros "(%R&%εa & %εb & %Hred &%Hbound & %Hineq & %Hpgl & Hlift)".
+        iIntros "( %εb & %Hred &%Hbound & %Hineq &  Hlift)".
         iApply (step_fupdN_mono _ _ _ (⌜SeriesC
            (prim_step chosen_e σ2 ≫= λ '(e3, σ3, efs),
                  sch_pexec sch n (ζ', (e :: <[length l1:=e3]> (l1 ++ chosen_e :: l2) ++ efs, σ3))) >=
-                                         1 - (εa + Expval (prim_step chosen_e σ2) εb)⌝)).
+                                         1 - (0 + Expval (prim_step chosen_e σ2) εb)⌝)).
         { iPureIntro. simpl in *.
           intros. etrans; first exact.
           apply Rle_ge.
           apply Ropp_le_cancel.
-          rewrite !Ropp_minus_distr. by apply Rplus_le_compat_r. }
+          rewrite !Ropp_minus_distr.
+          rewrite Rplus_0_l. by apply Rplus_le_compat_r. }
         iApply (safety_dbind_adv' _ _ _ _ (S n) with "[][][]").
         * iPureIntro. eapply mixin_prim_step_mass; [apply con_language_mixin|done].
         * iPureIntro. naive_solver.
-        * done.
+        * iPureIntro. by apply pgl_trivial.
         * iIntros (((e' & σ') & efs) HR).
-          iMod ("Hlift" with "[//]").
+          iMod ("Hlift" $! _ _ _).
           simpl.
           do 3 iModIntro.
           iApply (state_step_coupl_erasure_safety with "[$]").
diff --git a/theories/coneris/error_rules.v b/theories/coneris/error_rules.v
index 478d84cc..a6d91b22 100644
--- a/theories/coneris/error_rules.v
+++ b/theories/coneris/error_rules.v
@@ -168,7 +168,7 @@ Proof.
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr") as %(?&?& -> & He).
   iApply state_step_coupl_ret.
-  iApply prog_coupl_prim_step. 
+  iApply prog_coupl_prim_step; first (iModIntro; iIntros; by iApply state_step_coupl_ret_err_ge_1).
   iExists
       (λ ρ ,
         ∃ (n : fin (S (Z.to_nat z))), n ≠ m /\ ρ = (Val #n, σ1, [])), _, _.
@@ -220,7 +220,7 @@ Proof.
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr ") as %(?&?&->&He).
   iApply state_step_coupl_ret.
-  iApply prog_coupl_prim_step.
+  iApply prog_coupl_prim_step; first (iModIntro; iIntros; by iApply state_step_coupl_ret_err_ge_1).
   iExists
       (λ ρ ,
         ∃ (n : fin (S (Z.to_nat z))), fin_to_nat n ≠ m /\ ρ = (Val #n, σ1, [])),_,_.
@@ -268,7 +268,7 @@ Proof.
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr") as %(?&?&->&He).
   iApply state_step_coupl_ret.
-  iApply prog_coupl_prim_step.
+  iApply prog_coupl_prim_step; first (iModIntro; iIntros; by iApply state_step_coupl_ret_err_ge_1).
   iExists
     (λ ρ ,
       ∃ (n : fin (S (Z.to_nat z))), Forall (λ m, fin_to_nat n ≠ m) ns /\ ρ = (Val #n, σ1, [])),_,_.
@@ -314,7 +314,7 @@ Proof.
   iIntros "Hclose'".
   iDestruct (ec_supply_ec_inv with "Hε Herr ") as %(?&?&->&He).
   iApply state_step_coupl_ret.
-  iApply prog_coupl_prim_step.
+  iApply prog_coupl_prim_step; first (iModIntro; iIntros; by iApply state_step_coupl_ret_err_ge_1).
   iExists
     (λ ρ,
       ∃ (n : fin (S (Z.to_nat z))), Forall (λ m, Z.of_nat (fin_to_nat n) ≠ m) zs /\ ρ = (Val #n, σ1, [])),_,_.
@@ -412,7 +412,7 @@ Proof.
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iApply state_step_coupl_ret.
-  iApply prog_coupl_adv_comp; simpl.
+  iApply prog_coupl_adv_comp; simpl; first (iModIntro; iIntros; by iApply state_step_coupl_ret_err_ge_1).
   (* iDestruct (ec_supply_bound with "Hε Herr") as %?. *)
   iDestruct (ec_supply_ec_inv with "Hε Herr") as %(ε1' & ε3 & Hε_now & Hε1').
   unshelve eset (foo := (λ (ρ : expr * state * list expr),
diff --git a/theories/coneris/lifting.v b/theories/coneris/lifting.v
index 4a69eb54..27abc5fb 100644
--- a/theories/coneris/lifting.v
+++ b/theories/coneris/lifting.v
@@ -55,6 +55,7 @@ Section lifting.
     iApply state_step_coupl_ret.
     rewrite H.
     iApply prog_coupl_prim_step.
+    { iModIntro. iIntros. by iApply state_step_coupl_ret_err_ge_1. }
     iExists _.
     iExists nnreal_zero.
     iExists ε.
diff --git a/theories/coneris/weakestpre.v b/theories/coneris/weakestpre.v
index 5e3cc2ac..860e1ef0 100644
--- a/theories/coneris/weakestpre.v
+++ b/theories/coneris/weakestpre.v
@@ -40,12 +40,11 @@ Section modalities.
       ⌜(1<=ε)%R⌝ ∨
         Z σ1 ε ∨
         (∀ (ε':nonnegreal), ⌜(ε<ε')%R⌝ -∗ Φ (σ1, ε')) ∨
-      (∃ R μ (ε1 : nonnegreal) (ε2 : state con_prob_lang -> nonnegreal),
+      (∃ μ (ε2 : state con_prob_lang -> nonnegreal),
           ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
-          ⌜ (ε1 + Expval μ ε2 <= ε)%R ⌝ ∗
-          ⌜pgl μ R ε1⌝ ∗
-          ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ Φ (σ2, ε2 σ2)))%I.
+          ⌜ (Expval μ ε2 <= ε)%R ⌝ ∗
+          ∀ σ2, |={∅}=> Φ (σ2, ε2 σ2)))%I.
 
     
   #[local] Instance state_step_coupl_pre_ne Z Φ :
@@ -59,7 +58,7 @@ Section modalities.
   Proof.
     split; [|apply _].
     iIntros (Φ Ψ HNEΦ HNEΨ) "#Hwand".
-    iIntros ([??]) "[H|[?|[H|(%&%&%&%&%&%&%&%&H)]]]".
+    iIntros ([??]) "[H|[?|[H|(%&%&%&%&%&H)]]]".
     - by iLeft.
     - iRight; by iLeft.
     - iRight; iRight; iLeft.
@@ -68,7 +67,7 @@ Section modalities.
       by iApply "H".
     - do 3 iRight.
       repeat iExists _; repeat (iSplit; [done|]).
-      iIntros (??).
+      iIntros (?).
       iApply "Hwand".
       by iApply "H".
   Qed.
@@ -81,12 +80,11 @@ Section modalities.
       (⌜(1 <= ε)%R⌝ ∨
          (Z σ1 ε) ∨
          (∀ ε', ⌜(ε<ε')%R⌝ -∗ state_step_coupl σ1 ε' Z) ∨
-      (∃ R μ (ε1 : nonnegreal) (ε2 : state con_prob_lang -> nonnegreal),
+      (∃ μ (ε2 : state con_prob_lang -> nonnegreal),
           ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
-          ⌜ (ε1 + SeriesC (λ ρ, (μ ρ) * ε2 ρ) <= ε)%R ⌝ ∗
-          ⌜pgl μ R ε1⌝ ∗
-          ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ state_step_coupl σ2 (ε2 σ2) Z))%I.
+          ⌜ (SeriesC (λ ρ, (μ ρ) * ε2 ρ) <= ε)%R ⌝ ∗
+          ∀ σ2, |={∅}=> state_step_coupl σ2 (ε2 σ2) Z))%I.
   Proof. rewrite /state_step_coupl /state_step_coupl' least_fixpoint_unfold //. Qed.
 
   Lemma state_step_coupl_ret_err_ge_1 σ1 Z (ε : nonnegreal) :
@@ -115,6 +113,76 @@ Section modalities.
   Qed. 
 
   Lemma state_step_coupl_rec σ1 (ε : nonnegreal) Z :
+    (∃ μ (ε2 : state con_prob_lang -> nonnegreal),
+          ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
+          ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
+          ⌜ (Expval μ ε2 <= ε)%R ⌝ ∗
+          ∀ σ2, |={∅}=> state_step_coupl σ2 (ε2 σ2) Z)%I
+    ⊢ state_step_coupl σ1 ε Z.
+  Proof. iIntros "H". rewrite state_step_coupl_unfold. repeat iRight. done. Qed.
+
+  Lemma state_step_coupl_rec_equiv σ1 (ε : nonnegreal) Z :
+    (∃ μ (ε2 : state con_prob_lang -> nonnegreal),
+        ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
+        ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
+                    ⌜ (Expval μ ε2 <= ε)%R ⌝ ∗
+                    ∀ σ2, |={∅}=> state_step_coupl σ2 (ε2 σ2) Z)%I ⊣⊢
+    (∃ R μ (ε1 : nonnegreal) (ε2 : state con_prob_lang -> nonnegreal),
+        ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
+        ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
+                    ⌜ (ε1 + Expval μ ε2 <= ε)%R ⌝ ∗
+                    ⌜pgl μ R ε1⌝ ∗
+                    ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ state_step_coupl σ2 (ε2 σ2) Z)%I.
+  Proof.
+    iSplit.
+    - iIntros "H".
+      iDestruct "H" as "(%μ & %ε2 & % & [%r %] & %Hineq  &H)".
+      iExists (λ _, True), μ, 0, (λ σ, if bool_decide (μ σ > 0)%R then ε2 σ else 1).
+      repeat iSplit; first done.
+      + iPureIntro. exists (Rmax r 1).
+        intros; case_bool_decide.
+        * etrans; last apply Rmax_l. done.
+        * simpl. apply Rmax_r.
+      + simpl. iPureIntro. rewrite Rplus_0_l. etrans; last exact.
+        rewrite /Expval. apply Req_le.
+        apply SeriesC_ext.
+        intros n. case_bool_decide; first done.
+        destruct (pmf_pos μ n) as [K|K].
+        * exfalso. apply Rlt_gt in K. naive_solver.
+        * simpl. rewrite -K. lra.
+      + iPureIntro. by apply pgl_trivial.
+      + iIntros. case_bool_decide; first done.
+        by iApply state_step_coupl_ret_err_ge_1.
+    - iIntros "H".
+      iDestruct "H" as "(%R & %μ & %ε1 & %ε2 & % & [%r %] & %Hineq & %Hpgl &H)".
+      iExists μ, (λ σ, if bool_decide(R σ) then ε2 σ else 1).
+      repeat iSplit; try done.
+      + iPureIntro. exists (Rmax r 1).
+        intros; case_bool_decide.
+        * etrans; last apply Rmax_l. done.
+        * simpl. apply Rmax_r.
+      + rewrite /Expval in Hineq. rewrite /Expval. iPureIntro.
+        rewrite /pgl/prob in Hpgl. etrans; last exact.
+        etrans; last (apply Rplus_le_compat_r; exact).
+        rewrite -SeriesC_plus.
+        * apply SeriesC_le.
+          -- intros. split; first (case_bool_decide; real_solver).
+             case_bool_decide; simpl; try lra.
+             rewrite Rmult_1_r. apply Rplus_le_0_compat.
+             real_solver.
+          -- apply ex_seriesC_plus.
+             ++ apply (ex_seriesC_le _ μ); last done.
+                intros. case_bool_decide; by simpl.
+             ++ apply pmf_ex_seriesC_mult_fn. naive_solver.
+        * apply (ex_seriesC_le _ μ); last done.
+          intros. case_bool_decide; by simpl.
+        * apply pmf_ex_seriesC_mult_fn. naive_solver.
+      + iIntros. case_bool_decide.
+        * iApply ("H" with "[//]").
+        * by iApply state_step_coupl_ret_err_ge_1.
+  Qed.
+
+  Lemma state_step_coupl_rec' σ1 (ε : nonnegreal) Z :
     (∃ R μ (ε1 : nonnegreal) (ε2 : state con_prob_lang -> nonnegreal),
           ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
@@ -122,7 +190,10 @@ Section modalities.
           ⌜pgl μ R ε1⌝ ∗
           ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ state_step_coupl σ2 (ε2 σ2) Z)%I
     ⊢ state_step_coupl σ1 ε Z.
-  Proof. iIntros "H". rewrite state_step_coupl_unfold. repeat iRight. done. Qed.
+  Proof.
+    iIntros. iApply state_step_coupl_rec. by rewrite state_step_coupl_rec_equiv.
+  Qed.
+      
 
   Lemma state_step_coupl_ind (Ψ Z : state con_prob_lang → nonnegreal → iProp Σ) :
     ⊢ (□ (∀ σ ε,
@@ -145,7 +216,7 @@ Section modalities.
     (|={∅}=> state_step_coupl σ1 ε Z) ⊢ state_step_coupl σ1 ε Z.
   Proof.
     iIntros "H".
-    iApply state_step_coupl_rec.
+    iApply state_step_coupl_rec'.
     iExists (λ x, x= σ1), (dret σ1), nnreal_zero, (λ _, ε).
     repeat iSplit.
     - iPureIntro. apply dret_sch_erasable.
@@ -166,7 +237,7 @@ Section modalities.
     iRevert (σ1 ε) "Hs".
     iApply state_step_coupl_ind.
     iIntros "!#" (σ ε)
-      "[% | [? | [H|(% & % & % & % & % & % & % & % & H)]]] Hw".
+      "[% | [? | [H|(% & % & % & % & % & H)]]] Hw".
     - iApply state_step_coupl_ret_err_ge_1. lra.
     - iApply state_step_coupl_ret. by iApply "Hw".
     - iApply state_step_coupl_ampl.
@@ -175,8 +246,8 @@ Section modalities.
     - iApply state_step_coupl_rec.
       repeat iExists _.
       repeat iSplit; try done.
-      iIntros (??).
-      iMod ("H" with "[//]") as "[IH _]".
+      iIntros (?).
+      iMod ("H" $! σ2) as "[IH _]".
       by iApply "IH".
   Qed.
 
@@ -184,7 +255,7 @@ Section modalities.
     (ε1 <= ε2)%R → state_step_coupl σ1 ε1 Z -∗ state_step_coupl σ1 ε2 Z.
   Proof.
     iIntros (Heps) "Hs".
-    iApply state_step_coupl_rec.
+    iApply state_step_coupl_rec'.
     set (ε' := nnreal_minus ε2 ε1 Heps).
     iExists (λ x, x=σ1), (dret σ1), nnreal_zero, (λ _, ε1).
     repeat iSplit.
@@ -205,7 +276,7 @@ Section modalities.
     iRevert (σ1 ε) "Hs".
     iApply state_step_coupl_ind.
     iIntros "!#" (σ ε)
-      "[% | [H | [H|(% & % & % & % & % & % & % & % & H)]]] HZ".
+      "[% | [H | [H|(% & % & % & % & % & H)]]] HZ".
     - by iApply state_step_coupl_ret_err_ge_1.
     - iApply ("HZ" with "H").
     - iApply state_step_coupl_ampl.
@@ -215,8 +286,8 @@ Section modalities.
     - iApply state_step_coupl_rec.
       repeat iExists _.
       repeat iSplit; try done.
-      iIntros (??).
-      iMod ("H" with "[//]") as "[H _]".
+      iIntros (?).
+      iMod ("H" $! _) as "[H _]".
       by iApply "H".
   Qed.
   
@@ -227,7 +298,7 @@ Section modalities.
     ⊢ state_step_coupl σ1 (ε + ε') Z.
   Proof.
     iIntros (Hin) "(%R&%&H)".
-    iApply state_step_coupl_rec.
+    iApply state_step_coupl_rec'.
     iExists R, (state_step σ1 α), ε, (λ _, ε').
     repeat iSplit; try done.
     - iPureIntro.
@@ -249,7 +320,7 @@ Section modalities.
       ⊢ state_step_coupl σ1 ε Z)%I.
   Proof.
     iIntros (Hin) "(%R & %ε1 & %ε2 & % & %Hε & % & H)".
-    iApply state_step_coupl_rec.
+    iApply state_step_coupl_rec'.
     iExists R, _, ε1, ε2.
     repeat iSplit; try done.
     - iPureIntro.
@@ -278,6 +349,17 @@ Section modalities.
   (** * One step prog coupl *)
 
   Definition prog_coupl e1 σ1 ε Z : iProp Σ :=
+    (∃ (ε2 : (expr con_prob_lang * state con_prob_lang * list (expr con_prob_lang)) -> nonnegreal),
+           ⌜reducible e1 σ1⌝ ∗
+           ⌜∃ r, ∀ ρ, (ε2 ρ <= r)%R ⌝ ∗
+           ⌜(Expval (prim_step e1 σ1) ε2 <= ε)%R⌝ ∗
+           (∀ e2 σ2 efs, |={∅}=>
+                         Z e2 σ2 efs (ε2 (e2, σ2, efs)))
+       )%I.
+  
+  Definition prog_coupl_equiv1 e1 σ1 ε Z:
+    (∀ e2 σ2 efs, Z e2 σ2 efs 1) -∗
+    prog_coupl e1 σ1 ε Z -∗
     (∃ R (ε1 : nonnegreal) (ε2 : (expr con_prob_lang * state con_prob_lang * list (expr con_prob_lang)) -> nonnegreal),
            ⌜reducible e1 σ1⌝ ∗
            ⌜∃ r, ∀ ρ, (ε2 ρ <= r)%R ⌝ ∗
@@ -285,8 +367,67 @@ Section modalities.
            ⌜pgl (prim_step e1 σ1) R ε1⌝ ∗
            (∀ e2 σ2 efs, ⌜R (e2, σ2, efs)⌝ ={∅}=∗
                          Z e2 σ2 efs (ε2 (e2, σ2, efs)))
-       )%I.
-  
+    )%I.
+  Proof.
+    rewrite /prog_coupl.
+    iIntros "H1 H".
+    iDestruct "H" as "(%ε2 & % & [%r %] & %Hineq  &H)".
+    iExists (λ _, True), 0, (λ x, if bool_decide (prim_step e1 σ1 x > 0)%R then ε2 x else 1).
+    repeat iSplit; first done.
+    - iPureIntro. exists (Rmax r 1).
+      intros; case_bool_decide.
+      + etrans; last apply Rmax_l. done.
+      + simpl. apply Rmax_r.
+    - simpl. iPureIntro. rewrite Rplus_0_l. etrans; last exact.
+      rewrite /Expval. apply Req_le.
+      apply SeriesC_ext.
+      intros n. case_bool_decide; first done.
+      destruct (pmf_pos (prim_step e1 σ1) n) as [K|K].
+      + exfalso. apply Rlt_gt in K. naive_solver.
+      + simpl. rewrite -K. lra.
+    - iPureIntro. by apply pgl_trivial.
+    - iIntros. case_bool_decide; done.
+  Qed.
+
+  Definition prog_coupl_equiv2 e1 σ1 ε Z:
+    (∀ e2 σ2 efs, Z e2 σ2 efs 1) -∗
+    (∃ R (ε1 : nonnegreal) (ε2 : (expr con_prob_lang * state con_prob_lang * list (expr con_prob_lang)) -> nonnegreal),
+        ⌜reducible e1 σ1⌝ ∗
+        ⌜∃ r, ∀ ρ, (ε2 ρ <= r)%R ⌝ ∗
+                   ⌜(ε1 + Expval (prim_step e1 σ1) ε2 <= ε)%R⌝ ∗
+                   ⌜pgl (prim_step e1 σ1) R ε1⌝ ∗
+                   (∀ e2 σ2 efs, ⌜R (e2, σ2, efs)⌝ ={∅}=∗
+                                 Z e2 σ2 efs (ε2 (e2, σ2, efs)))
+    )%I-∗
+    prog_coupl e1 σ1 ε Z.
+  Proof. 
+    iIntros "H1 H".
+    iDestruct "H" as "(%R & %ε1 & %ε2 & % & [%r %] & %Hineq & %Hpgl &H)".
+    iExists (λ σ, if bool_decide(R σ) then ε2 σ else 1).
+    repeat iSplit; try done.
+    - iPureIntro. exists (Rmax r 1).
+      intros; case_bool_decide.
+      + etrans; last apply Rmax_l. done.
+      + simpl. apply Rmax_r.
+    - rewrite /Expval in Hineq. rewrite /Expval. iPureIntro.
+      rewrite /pgl/prob in Hpgl. etrans; last exact.
+      etrans; last (apply Rplus_le_compat_r; exact).
+      rewrite -SeriesC_plus.
+      + apply SeriesC_le.
+        * intros. split; first (case_bool_decide; real_solver).
+          case_bool_decide; simpl; try lra.
+          rewrite Rmult_1_r. apply Rplus_le_0_compat.
+          real_solver.
+        * apply ex_seriesC_plus.
+          -- apply (ex_seriesC_le _ (prim_step e1 σ1)); last done.
+             intros. case_bool_decide; by simpl.
+          -- apply pmf_ex_seriesC_mult_fn. naive_solver.
+      + apply (ex_seriesC_le _ (prim_step e1 σ1)); last done.
+        intros. case_bool_decide; by simpl.
+      + apply pmf_ex_seriesC_mult_fn. naive_solver.
+    - iIntros. case_bool_decide; last done.
+      iApply ("H" with "[//]").
+  Qed. 
   (* Definition glm_pre *)
   (*   (Z : (expr con_prob_lang * state con_prob_lang * list (expr con_prob_lang)) -> nonnegreal -> iProp Σ) (Φ : partial_cfg con_prob_lang * nonnegreal -> iProp Σ) := *)
   (*   (λ (x : partial_cfg con_prob_lang * nonnegreal), *)
@@ -366,7 +507,7 @@ Section modalities.
   Lemma prog_coupl_mono_err e σ Z ε ε':
     (ε<=ε')%R -> prog_coupl e σ ε Z -∗ prog_coupl e σ ε' Z.
   Proof.
-    iIntros (?) "(%&%&%&%&%&%&%&H)".
+    iIntros (?) "(%&%&%&%&H)".
     repeat iExists _.
     repeat iSplit; try done.
     iPureIntro.
@@ -374,19 +515,30 @@ Section modalities.
   Qed.
 
   Lemma prog_coupl_strong_mono e1 σ1 Z1 Z2 ε :
+    □(∀ e2 σ2 efs, Z2 e2 σ2 efs 1) -∗
     (∀ e2 σ2 ε' efs, ⌜∃ σ, (prim_step e1 σ (e2, σ2, efs) > 0)%R⌝ ∗ Z1 e2 σ2 efs ε' -∗ Z2 e2 σ2 efs ε') -∗
     prog_coupl e1 σ1 ε Z1 -∗ prog_coupl e1 σ1 ε Z2.
   Proof.
-    iIntros "Hm (%&%&%&%&%&%&% & Hcnt) /=".
-    repeat iExists _. repeat iSplit.
-    - done.
-    - done.
+    iIntros "#H1 Hm (%&%&[%r %]&%Hineq & Hcnt) /=".
+    rewrite /prog_coupl.
+    iExists (λ x, if bool_decide (∃ σ, prim_step e1 σ x >0)%R then ε2 x else 1).
+    repeat iSplit.
     - done.
-    - iPureIntro; by apply pgl_pos_R.
-    - simpl. iIntros (???[??]).
-      iApply "Hm".
-      iSplitR; [by iExists _|].
-      by iApply "Hcnt".
+    - iPureIntro. exists (Rmax r 1).
+      intros; case_bool_decide.
+      + etrans; last apply Rmax_l. done.
+      + simpl. apply Rmax_r.
+    - rewrite /Expval in Hineq. rewrite /Expval. iPureIntro.
+      rewrite /Expval. etrans; last exact. apply Req_le.
+      apply SeriesC_ext.
+      intros n. case_bool_decide; first done.
+      destruct (pmf_pos (prim_step e1 σ1) n) as [K|K].
+      + exfalso. apply Rlt_gt in K. naive_solver.
+      + simpl. rewrite -K. lra.
+    - simpl. iIntros (???).
+      case_bool_decide; last done.
+      iApply "Hm". iMod ("Hcnt" $! _ _ _).
+      by iFrame.
   Qed.
 
   Lemma prog_coupl_mono e1 σ1 Z1 Z2 ε :
@@ -394,8 +546,10 @@ Section modalities.
     prog_coupl e1 σ1 ε Z1 -∗ prog_coupl e1 σ1 ε Z2.
   Proof.
     iIntros "Hm".
-    iApply prog_coupl_strong_mono.
-    iIntros (????) "[_ H]". by iApply "Hm".
+    rewrite /prog_coupl.
+    iIntros "(%&%&%&%&?)".
+    repeat iExists _; repeat iSplit; try done.
+    iIntros. by iApply "Hm".
   Qed.
   
   (* Lemma glm_mono_grading e σ Z ε ε' : *)
@@ -498,10 +652,33 @@ Section modalities.
   (* Qed. *)
 
   Lemma prog_coupl_strengthen e1 σ1 Z ε :
+    □(∀ e2 σ2 efs, Z e2 σ2 efs 1) -∗
     prog_coupl e1 σ1 ε Z -∗
-    prog_coupl e1 σ1 ε (λ e2 σ2 efs ε', ⌜∃ σ, (prim_step e1 σ (e2, σ2, efs) > 0)%R⌝ ∧ Z e2 σ2 efs ε').
+    prog_coupl e1 σ1 ε (λ e2 σ2 efs ε', ⌜(∃ σ, (prim_step e1 σ (e2, σ2, efs) > 0)%R)\/ (1<=ε')%R⌝ ∧ Z e2 σ2 efs ε').
   Proof.
-    iApply prog_coupl_strong_mono. iIntros (????) "[$ $]".
+    iIntros "#Hmono (%&%&[%r %]&%Hineq & Hcnt) /=".
+    rewrite /prog_coupl.
+    iExists (λ x, if bool_decide (∃ σ, prim_step e1 σ x >0)%R then ε2 x else 1).
+    repeat iSplit.
+    - done.
+    - iPureIntro. exists (Rmax r 1).
+      intros; case_bool_decide.
+      + etrans; last apply Rmax_l. done.
+      + simpl. apply Rmax_r.
+    - rewrite /Expval in Hineq. rewrite /Expval. iPureIntro.
+      rewrite /Expval. etrans; last exact. apply Req_le.
+      apply SeriesC_ext.
+      intros n. case_bool_decide; first done.
+      destruct (pmf_pos (prim_step e1 σ1) n) as [K|K].
+      + exfalso. apply Rlt_gt in K. naive_solver.
+      + simpl. rewrite -K. lra.
+    - simpl. iIntros (???).
+      case_bool_decide.
+      + iMod ("Hcnt" $! _ _ _).
+        iFrame. iPureIntro. naive_solver.
+      + iMod ("Hcnt" $! e2 σ2 efs ).
+        iModIntro. iSplit; last iApply "Hmono".
+        iPureIntro. naive_solver.
   Qed.
   
   (* Lemma glm_strengthen e1 σ1 Z ε : *)
@@ -514,23 +691,27 @@ Section modalities.
 
   Lemma prog_coupl_ctx_bind K `{!ConLanguageCtx K} e1 σ1 Z ε:
     to_val e1 = None ->
+    □(∀ e2 σ2 efs, Z e2 σ2 efs 1) -∗
     prog_coupl e1 σ1 ε (λ e2 σ2 efs ε', Z (K e2) σ2 efs ε') -∗ prog_coupl (K e1) σ1 ε Z.
   Proof.
-    iIntros (Hv) "(%R&%ε1&%ε2&%&[%r %]&%&%&H)".
-    
+    iIntros (Hv) "#H' H".
+    (* iDestruct (prog_coupl_strengthen with "[][$]") as "H". *)
+    (* { iModIntro. by iIntros. } *)
+    iDestruct "H" as "(%ε2&%&[%r %]&%&H)".
     (** (classical) inverse of context [K] *)
     destruct (partial_inv_fun K) as (Kinv & HKinv).
     assert (∀ e, Kinv (K e) = Some e) as HKinv3.
     { intro e.
       destruct (Kinv (K e)) eqn:Heq;
         eapply HKinv in Heq; by simplify_eq. }
-    set (ε2' := (λ '(e, σ, efs), from_option (λ e', ε2 (e', σ, efs)) 0%NNR (Kinv e))).
+    set (ε2' := (λ '(e, σ, efs), from_option (λ e', ε2 (e', σ, efs)) 1%NNR (Kinv e))).
     assert (∀ e2 σ2 efs, ε2' (K e2, σ2, efs) = ε2 (e2, σ2, efs)) as Hε2'.
     { intros. rewrite /ε2' HKinv3 //. }
-    iExists (λ '(e2, σ2, efs), ∃ e2', e2 = K e2' /\ R (e2', σ2, efs)), ε1, ε2'.
+    (* iExists (λ '(e2, σ2, efs), ∃ e2', e2 = K e2' /\ R (e2', σ2, efs)), ε1, ε2'. *)
+    iExists ε2'.
     repeat iSplit; try iPureIntro.
     - by apply reducible_fill.
-    - rewrite /ε2'. eexists (Rmax 0%R r).
+    - rewrite /ε2'. eexists (Rmax 1%R r).
       intros [[??]?].
       destruct (Kinv _); simpl.
       + etrans; last apply Rmax_r. done.
@@ -538,25 +719,25 @@ Section modalities.
     - rewrite fill_dmap// Expval_dmap//=; last first.
       + eapply ex_expval_bounded. simpl. intros [[??]?] => /=. by rewrite HKinv3/=.
       + etrans; last done.
-        apply Rle_plus_plus; first done.
-        right.
+        rewrite /Expval. apply Req_le.
         apply SeriesC_ext.
         intros [[??]?]. simpl. by rewrite HKinv3/=.
-    - rewrite fill_dmap//.
-      replace (ε1) with (ε1+0)%NNR; last (apply nnreal_ext; simpl; lra).
-      eapply pgl_dbind; try done.
-      intros a ?. apply pgl_dret.
-      destruct a as [[??]?] => /=.
-      naive_solver.
-    - iIntros (???(?&->&?)).
-      rewrite /ε2'. rewrite HKinv3/=.
-      by iApply "H".
+    (* - rewrite fill_dmap//. *)
+    (*   replace (ε1) with (ε1+0)%NNR; last (apply nnreal_ext; simpl; lra). *)
+    (*   eapply pgl_dbind; try done. *)
+    (*   intros a ?. apply pgl_dret. *)
+    (*   destruct a as [[??]?] => /=. *)
+    (*   naive_solver. *)
+    - iIntros (???).
+      rewrite /ε2'.
+      destruct (Kinv e2) eqn:H'; simpl; last done.
+      apply HKinv in H'. by subst.
   Qed.
 
   
   Lemma prog_coupl_reducible e σ Z ε :
     prog_coupl e σ ε Z -∗ ⌜reducible e σ⌝.
-  Proof. by iIntros "(%&%&%&%&%&%&%& _)". Qed.
+  Proof. by iIntros "(%&%&%&%& _)". Qed.
   
   (* Lemma glm_bind K `{!ConLanguageCtx K} e1 σ1 Z ε : *)
   (*   to_val e1 = None → *)
@@ -693,12 +874,28 @@ Section modalities.
   (* Qed. *)
 
 
+  Lemma prog_coupl_adv_comp e1 σ1 Z (ε : nonnegreal) :
+    □(∀ e2 σ2 efs, Z e2 σ2 efs 1) -∗
+      (∃ R (ε1 : nonnegreal) (ε2 : _ -> nonnegreal),
+          ⌜reducible e1 σ1⌝ ∗
+          ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
+          ⌜ (ε1 + Expval (prim_step e1 σ1) ε2 <= ε)%R ⌝ ∗ ⌜pgl (prim_step e1 σ1) R ε1⌝ ∗
+          ∀ e2 σ2 efs, ⌜ R (e2, σ2, efs) ⌝ ={∅}=∗ Z e2 σ2 efs (ε2 (e2, σ2, efs))) -∗
+        prog_coupl e1 σ1 ε Z.
+  Proof.
+    iIntros "#H' H".
+    by iApply prog_coupl_equiv2.
+  Qed.
+
   Lemma prog_coupl_prim_step e1 σ1 Z ε :
+    □(∀ e2 σ2 efs, Z e2 σ2 efs 1) -∗
     (∃ R ε1 ε2, ⌜reducible e1 σ1⌝ ∗ ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜pgl (prim_step e1 σ1) R ε1⌝ ∗
-          ∀ e2 σ2 efs, ⌜R (e2, σ2, efs)⌝ ={∅}=∗ Z e2 σ2 efs ε2)
-    ⊢ prog_coupl e1 σ1 ε Z.
+          ∀ e2 σ2 efs, ⌜R (e2, σ2, efs)⌝ ={∅}=∗ Z e2 σ2 efs ε2) -∗
+     prog_coupl e1 σ1 ε Z.
   Proof.
-    iIntros "(%R&%ε1&%ε2&%&%&%&H)".
+    iIntros "#H' H".
+    iApply prog_coupl_adv_comp; first done.
+    iDestruct "H" as "(%R&%ε1 & %ε2 & % & %& % & H)".
     iExists R, ε1, (λ _, ε2).
     repeat iSplit; try done.
     - iPureIntro. naive_solver.
@@ -706,19 +903,6 @@ Section modalities.
       rewrite prim_step_mass; [lra|done].
   Qed. 
 
-  Lemma prog_coupl_adv_comp e1 σ1 Z (ε : nonnegreal) :
-      (∃ R (ε1 : nonnegreal) (ε2 : _ -> nonnegreal),
-          ⌜reducible e1 σ1⌝ ∗
-          ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
-          ⌜ (ε1 + Expval (prim_step e1 σ1) ε2 <= ε)%R ⌝ ∗ ⌜pgl (prim_step e1 σ1) R ε1⌝ ∗
-            ∀ e2 σ2 efs, ⌜ R (e2, σ2, efs) ⌝ ={∅}=∗ Z e2 σ2 efs (ε2 (e2, σ2, efs)))
-    ⊢ prog_coupl e1 σ1 ε Z.
-  Proof.
-    iIntros "(% & % & % & % & % & % & % & H)".
-    iExists _,_,_.
-    by repeat iSplit.
-  Qed.
-
 
   (* Lemma glm_strong_ind (Ψ : expr con_prob_lang → state con_prob_lang → nonnegreal → iProp Σ) Z : *)
   (*   (∀ n e σ ε, Proper (dist n) (Ψ e σ ε)) → *)
@@ -770,7 +954,7 @@ Proof.
   rewrite /state_step_coupl_pre.
   do 3 f_equiv.
   rewrite /prog_coupl.
-  do 18 f_equiv.
+  do 12 f_equiv.
   f_contractive.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [[??]?].
@@ -812,7 +996,7 @@ Proof.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [[]?]. rewrite /state_step_coupl_pre.
   rewrite /prog_coupl.
-  do 21 f_equiv.
+  do 15 f_equiv.
   f_contractive.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [[]?]. rewrite /state_step_coupl_pre.
@@ -835,7 +1019,7 @@ Proof.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [[]?]. rewrite /state_step_coupl_pre.
   rewrite /prog_coupl.
-  do 20 f_equiv.
+  do 14 f_equiv.
   f_contractive. 
   apply least_fixpoint_ne_outer; [|done].
   intros ? [[]?]. rewrite /state_step_coupl_pre.
@@ -947,9 +1131,11 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   - iIntros ">(?&?&>?)". by iFrame.
   - iIntros "H".
-    iDestruct (prog_coupl_strengthen with "H") as "H".
+    iDestruct (prog_coupl_strengthen with "[]H") as "H".
+    { iModIntro. iIntros. by iApply state_step_coupl_ret_err_ge_1. }
     iApply (prog_coupl_mono with "[] [$]").
-    iIntros (????) "[[%%Hstep]?]!>".
+    iIntros (????) "[[[%%H]|%]?]!>"; last first.
+    { by iApply state_step_coupl_ret_err_ge_1. }
     iApply (state_step_coupl_bind with "[][$]").
     iIntros (??) "H".
     iApply fupd_state_step_coupl.
@@ -959,12 +1145,12 @@ Proof.
     iMod "H". iModIntro.
     iApply (state_step_coupl_mono with "[-H]H").
     iIntros (??).
-    case_match eqn:H.
+    case_match eqn:H'.
     + iIntros ">(?&?&>?)".
       iFrame. iModIntro.
-      rewrite -(of_to_val _ _ H).
+      rewrite -(of_to_val _ _ H').
       by iApply pgl_wp_value_fupd'.
-    + pose proof (atomic _ _ _ _ Hstep) as [??].
+    + pose proof (atomic _ _ _ _ H) as [??].
       congruence.
 Qed. 
 
@@ -1009,7 +1195,8 @@ Proof.
   }
   rewrite fill_not_val; last done.
   iApply state_step_coupl_ret.
-  iApply prog_coupl_ctx_bind; first done.
+  iApply prog_coupl_ctx_bind; [done|..].
+  { iModIntro; iIntros. by iApply state_step_coupl_ret_err_ge_1. }
   iApply (prog_coupl_mono with "[] [$]").
   iIntros (????) "H!>".
   iApply (state_step_coupl_mono with "[][$]").