diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean b/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean
index b933cf9..53d7b00 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean
@@ -181,8 +181,8 @@ def WfD.CongD.right {P : Ctx α ε → LCtx α → Region φ → Region φ → S
 
 inductive TStepD : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) → Type _
   -- TODO: do we need to require r.WfD for rw?
-  | step {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → StepD Γ.effect r r' → TStepD Γ L r r'
-  | step_op {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → StepD Γ.effect r' r → TStepD Γ L r r'
+  | step {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → FStepD Γ.effect r r' → TStepD Γ L r r'
+  | step_op {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → FStepD Γ.effect r' r → TStepD Γ L r r'
   | initial {Γ L} : Γ.IsInitial → r.WfD Γ L → r'.WfD Γ L → TStepD Γ L r r'
   | terminal {Γ L} : e.WfD Γ ⟨Ty.unit, ⊥⟩ → e'.WfD Γ ⟨Ty.unit, ⊥⟩ → r.WfD (⟨Ty.unit, ⊥⟩::Γ) L
     → TStepD Γ L (let1 e r) (let1 e' r)
@@ -194,8 +194,8 @@ def TStepD.symm {Γ L} {r r' : Region φ} : TStepD Γ L r r' → TStepD Γ L r'
   | terminal e e' d => terminal e' e d
 
 inductive TStep : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) → Prop
-  | step {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → StepD Γ.effect r r' → TStep Γ L r r'
-  | step_op {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → StepD Γ.effect r' r → TStep Γ L r r'
+  | step {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → FStep Γ.effect r r' → TStep Γ L r r'
+  | step_op {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → FStep Γ.effect r' r → TStep Γ L r r'
   | initial {Γ L} : Γ.IsInitial → r.Wf Γ L → r'.Wf Γ L → TStep Γ L r r'
   | terminal {Γ L} : e.Wf Γ ⟨Ty.unit, ⊥⟩ → e'.Wf Γ ⟨Ty.unit, ⊥⟩ → r.Wf (⟨Ty.unit, ⊥⟩::Γ) L
     → TStep Γ L (let1 e r) (let1 e' r)
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean
index 907ee94..560b05e 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean
@@ -247,8 +247,8 @@ def RewriteD.lsubst_alpha {r₀ r₀'}
     exact hρ
     rw [Subst.vlift_liftn_comm]
     rfl
-  | let2_eta r => by
-    apply cast_src _ (let2_eta _)
+  | let2_eta e r => by
+    apply cast_src _ (let2_eta _ _)
     simp only [lsubst]
     congr
     simp only [vlift_alpha, vwk_vwk, vliftn_alpha, <-Nat.liftWk_comp, vwk1_lsubst_alpha]
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
index fd24ace..11f01c3 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
@@ -294,6 +294,33 @@ theorem Term.wk_comp (ρ σ)
 
 def Term.wk1 : Term φ → Term φ := wk (Nat.liftWk Nat.succ)
 
+theorem Term.wk_wk1 (r : Term φ) : r.wk1.wk ρ = r.wk (ρ ∘ Nat.liftWk Nat.succ)
+  := by simp only [wk1, wk_wk, <-Nat.liftWk_comp]
+
+theorem Term.wk_liftWk₂_wk1_to_wk (r : Term φ)
+  : r.wk1.wk (Nat.liftWk (Nat.liftWk ρ)) = r.wk (Nat.liftWk (Nat.succ ∘ ρ))
+  := by rw [wk_wk1, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
+
+theorem Term.wk_liftWk₂_wk1 (r : Term φ)
+  : r.wk1.wk (Nat.liftWk (Nat.liftWk ρ)) = (r.wk (Nat.liftWk ρ)).wk1
+  := by rw [wk_liftWk₂_wk1_to_wk, wk1, wk_wk, Nat.liftWk_comp]
+
+theorem Term.wk_liftnWk₂_wk1 (r : Term φ)
+  : r.wk1.wk (Nat.liftnWk 2 ρ) = (r.wk (Nat.liftWk ρ)).wk1
+  := by rw [Nat.liftnWk_two, <-wk_liftWk₂_wk1]; rfl
+
+theorem Term.wk1_wk_liftWk (r : Term φ)
+  : (r.wk (Nat.liftWk ρ)).wk1 = r.wk1.wk (Nat.liftnWk 2 ρ)
+  := r.wk_liftnWk₂_wk1.symm
+
+theorem Term.wk_liftWk_wk_succ (r : Term φ)
+  :  (r.wk Nat.succ).wk (Nat.liftWk ρ) = (r.wk ρ).wk Nat.succ
+  := by simp only [wk_wk, Nat.liftWk_comp_succ]
+
+theorem Term.wk_liftnWk_wk_add (r : Term φ) (n : ℕ)
+  :  (r.wk (· + n)).wk (Nat.liftnWk n ρ) = (r.wk ρ).wk (· + n)
+  := by simp only [wk_wk, Nat.liftnWk_comp_add]
+
 def Term.wkn (n : ℕ) : Term φ → Term φ := wk (Nat.liftWk (· + n))
 
 theorem Body.wk_id (b : Body φ) : b.wk id = b := by induction b <;> simp [*]
@@ -663,6 +690,30 @@ theorem Region.vwk_comp (ρ σ)
 
 def Region.vwk1 : Region φ → Region φ := vwk (Nat.liftWk Nat.succ)
 
+theorem Region.vwk_vwk1 (r : Region φ) : r.vwk1.vwk ρ = r.vwk (ρ ∘ Nat.liftWk Nat.succ)
+  := by simp only [vwk1, vwk_vwk, <-Nat.liftWk_comp]
+
+theorem Region.vwk_liftWk₂_vwk1_to_vwk (r : Region φ)
+  : r.vwk1.vwk (Nat.liftWk (Nat.liftWk ρ)) = r.vwk (Nat.liftWk (Nat.succ ∘ ρ))
+  := by rw [vwk_vwk1, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
+
+theorem Region.vwk_liftWk₂_vwk1 (r : Region φ)
+  : r.vwk1.vwk (Nat.liftWk (Nat.liftWk ρ)) = (r.vwk (Nat.liftWk ρ)).vwk1
+  := by rw [vwk_liftWk₂_vwk1_to_vwk, vwk1, vwk_vwk, Nat.liftWk_comp]
+
+theorem Region.vwk_liftnWk₂_vwk1 (r : Region φ)
+  : r.vwk1.vwk (Nat.liftnWk 2 ρ) = (r.vwk (Nat.liftWk ρ)).vwk1
+  := by rw [Nat.liftnWk_two, <-vwk_liftWk₂_vwk1]; rfl
+
+theorem Region.vwk1_vwk_liftWk (r : Region φ)
+  : (r.vwk (Nat.liftWk ρ)).vwk1 = r.vwk1.vwk (Nat.liftnWk 2 ρ)
+  := r.vwk_liftnWk₂_vwk1.symm
+
+theorem Region.vwk_liftnWk₂_liftWk_vwk2 (r : Region φ)
+  : (r.vwk (Nat.liftnWk 2 Nat.succ)).vwk (Nat.liftnWk 2 (Nat.liftWk ρ))
+  = (r.vwk (Nat.liftnWk 2 ρ)).vwk (Nat.liftnWk 2 Nat.succ)
+  := by simp only [vwk_vwk, <-Nat.liftnWk_comp, Nat.liftWk_comp_succ]
+
 def Region.vwkn (n : ℕ) : Region φ → Region φ := vwk (Nat.liftWk (· + n))
 
 theorem Region.lwk_id (r : Region φ) : r.lwk id = r := by induction r <;> simp [*]
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Definitions.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Definitions.lean
index d1de33d..9d2ea10 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Definitions.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Definitions.lean
@@ -281,10 +281,10 @@ inductive RewriteD : Region φ → Region φ → Type _
   | cfg_let1 (a β n G) :
     RewriteD (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G))
   | cfg_let2 (a β n G) :
-    RewriteD (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
+    RewriteD (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
   | cfg_case (e r s n G) :
     RewriteD (cfg (case e r s) n G)
-      (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
+      (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
   | cfg_cfg (β n G n' G') :
     RewriteD (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
   | cfg_zero (β G) : RewriteD (cfg β 0 G) β
@@ -292,11 +292,9 @@ inductive RewriteD : Region φ → Region φ → Type _
     RewriteD
       (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
       (cfg β k (G ∘ ρ))
-  | let2_eta (r : Region φ) :
-    RewriteD (let2 (Term.var 0) (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
-      (let1 (Term.var 0) r)
-  -- | let1_eta r :
-  --   RewriteD (let1 (Term.var 0) r.vwk1) r
+  | let2_eta (e) (r : Region φ) :
+    RewriteD (let2 e (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
+      (let1 e r)
 
 def RewriteD.cast_src {r₀ r₀' r₁ : Region φ} (h : r₀ = r₀') (p : RewriteD r₀ r₁)
   : RewriteD r₀' r₁ := h ▸ p
@@ -365,9 +363,7 @@ theorem RewriteD.effect {Γ : ℕ → ε} {r r' : Region φ} (p : RewriteD r r')
     apply congrArg
     apply congrArg
     funext i
-    rw [
-      Nat.liftnBot_two_apply, <-Nat.liftnBot_two_apply, Function.comp_apply, effect_liftnBot_vwk_add
-    ]
+    simp [Nat.liftnBot_two]
   | cfg_case => simp [sup_assoc]
   | cfg_cfg =>
     simp only [effect_cfg, sup_assoc]
@@ -428,10 +424,10 @@ inductive Rewrite : Region φ → Region φ → Prop
   | cfg_let1 (a β n G) :
     Rewrite (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G))
   | cfg_let2 (a β n G) :
-    Rewrite (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
+    Rewrite (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
   | cfg_case (e r s n G) :
     Rewrite (cfg (case e r s) n G)
-      (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
+      (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
   | cfg_cfg (β n G n' G') :
     Rewrite (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
   | cfg_zero (β G) : Rewrite (cfg β 0 G) β
@@ -439,9 +435,9 @@ inductive Rewrite : Region φ → Region φ → Prop
     Rewrite
       (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
       (cfg β k (G ∘ ρ))
-  | let2_eta (r : Region φ) :
-    Rewrite (let2 (Term.var 0) (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
-      (let1 (Term.var 0) r)
+  | let2_eta (e) (r : Region φ) :
+    Rewrite (let2 e (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1))
+      (let1 e r)
 
 theorem RewriteD.rewrite {r r' : Region φ} (p : RewriteD r r') : Rewrite r r'
   := by cases p <;> constructor; assumption
@@ -543,12 +539,12 @@ theorem eqv_cfg_let1 {a β n G}
   := EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_let1 a β n G
 
 theorem eqv_cfg_let2 {a β n G}
-  : @cfg φ (let2 a β) n G ≈ (let2 a $ cfg β n (vwk (· + 2) ∘ G))
+  : @cfg φ (let2 a β) n G ≈ (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
   := EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_let2 a β n G
 
 theorem eqv_cfg_case {e r s n G}
   : @cfg φ (case e r s) n G
-    ≈ case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G))
+    ≈ case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
   := EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_case e r s n G
 
 theorem eqv_cfg_cfg {β n G n' G'}
@@ -560,10 +556,35 @@ theorem eqv_cfg_fuse {β n G k} (ρ : Fin k → Fin n) (hρ : Function.Surjectiv
     ≈ cfg β k (G ∘ ρ)
   := EqvGen.rel _ _ $ Cong.rel $ Rewrite.cfg_fuse β n G k ρ hρ
 
-theorem eqv_let2_eta {r : Region φ}
-  : @let2 φ (Term.var 0) (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1)
-    ≈ let1 (Term.var 0) r
-  := EqvGen.rel _ _ $ Cong.rel $ Rewrite.let2_eta r
+theorem eqv_let2_eta {e} {r : Region φ}
+  : @let2 φ e (let1 ((Term.var 1).pair (Term.var 0)) r.vwk1.vwk1)
+    ≈ let1 e r
+  := EqvGen.rel _ _ $ Cong.rel $ Rewrite.let2_eta e r
+
+def RewriteD.vwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : RewriteD (r.vwk ρ) (r'.vwk ρ)
+  := by cases d with
+  | let2_pair a b r =>
+    simp only [
+      Region.vwk, wk, Nat.liftWk, vwk_liftWk₂_vwk1, wk_liftWk_wk_succ, Nat.liftnWk_two]
+    constructor
+  | cfg_cfg β n G n' G' =>
+    simp only [Region.vwk, wk, Fin.comp_addCases_apply]
+    rw [<-Function.comp.assoc, Region.vwk_comp_lwk, Function.comp.assoc]
+    constructor
+  | cfg_fuse β n G k σ hσ =>
+    simp only [Region.vwk, Region.vwk_lwk, Function.comp_apply]
+    constructor
+    assumption
+  | let2_eta e r =>
+    simp only [Region.vwk, wk, Nat.liftnWk, Nat.lt_succ_self, ↓reduceIte, Nat.zero_lt_succ,
+      Nat.liftWk_comm_liftnWk_apply, vwk_liftnWk₂_vwk1, vwk_liftWk₂_vwk1]
+    constructor
+  | _ =>
+    simp only [
+      Region.vwk, wk, Nat.liftWk,
+      vwk_liftWk₂_vwk1, wk_liftWk_wk_succ, vwk_liftnWk₂_liftWk_vwk2, vwk_liftnWk₂_vwk1,
+      wk_liftnWk_wk_add, Nat.liftWk_comm_liftnWk_apply, Function.comp_apply]
+    constructor
 
 inductive ReduceD : Region φ → Region φ → Type _
   | case_inl (e r s) : ReduceD (case (inl e) r s) (let1 e r)
@@ -818,25 +839,25 @@ def StepD.cfg_let1_op {Γ : ℕ → ε} (a : Term φ) (β n G)
 
 @[match_pattern]
 def StepD.cfg_let2 {Γ : ℕ → ε} (a : Term φ) (β n G)
-  : StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
+  : StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
   := StepD.rw $ RewriteD.cfg_let2 a β n G
 
 @[match_pattern]
 def StepD.cfg_let2_op {Γ : ℕ → ε} (a : Term φ) (β n G)
-  : StepD Γ (let2 a $ cfg β n (vwk (· + 2) ∘ G))
+  : StepD Γ (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
     (cfg (let2 a β) n G)
   := StepD.rw_op $ RewriteD.cfg_let2 a β n G
 
 @[match_pattern]
 def StepD.cfg_case {Γ : ℕ → ε} (e : Term φ) (r s n G)
   : StepD Γ (cfg (case e r s) n G)
-    (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G))
+    (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
   )
   := StepD.rw $ RewriteD.cfg_case e r s n G
 
 @[match_pattern]
 def StepD.cfg_case_op {Γ : ℕ → ε} (e : Term φ) (r s n G)
-  : StepD Γ (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
+  : StepD Γ (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
     (cfg (case e r s) n G)
   := StepD.rw_op $ RewriteD.cfg_case e r s n G
 
@@ -860,14 +881,14 @@ def StepD.cfg_zero_op {Γ : ℕ → ε} (β : Region φ) (G)
   : StepD Γ β (cfg β 0 G) := StepD.rw_op $ RewriteD.cfg_zero β G
 
 @[match_pattern]
-def StepD.let2_eta {Γ : ℕ → ε} (r : Region φ)
-  : StepD Γ (let2 (var 0) (let1 ((var 1).pair (var 0)) r.vwk1.vwk1)) (let1 (var 0) r)
-  := StepD.rw $ RewriteD.let2_eta r
+def StepD.let2_eta {Γ : ℕ → ε} (e) (r : Region φ)
+  : StepD Γ (let2 e (let1 ((var 1).pair (var 0)) r.vwk1.vwk1)) (let1 e r)
+  := StepD.rw $ RewriteD.let2_eta e r
 
 @[match_pattern]
 def StepD.let2_eta_op {Γ : ℕ → ε} (r : Region φ)
-  : StepD Γ (let1 (var 0) r) (let2 (var 0) (let1 ((var 1).pair (var 0)) r.vwk1.vwk1))
-  := StepD.rw_op $ RewriteD.let2_eta r
+  : StepD Γ (let1 e r) (let2 e (let1 ((var 1).pair (var 0)) r.vwk1.vwk1))
+  := StepD.rw_op $ RewriteD.let2_eta e r
 
 -- @[match_pattern]
 -- def StepD.let1_eta {Γ : ℕ → ε} (r : Region φ)
@@ -1115,22 +1136,22 @@ def RWD.cfg_let1_op {Γ : ℕ → ε} (a : Term φ) (β n G)
   := single $ BCongD.rel $ StepD.cfg_let1_op a β n G
 
 def RWD.cfg_let2 {Γ : ℕ → ε} (a : Term φ) (β n G)
-  : RWD StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G))
+  : RWD StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
   := single $ BCongD.rel $ StepD.cfg_let2 a β n G
 
 def RWD.cfg_let2_op {Γ : ℕ → ε} (a : Term φ) (β n G)
-  : RWD StepD Γ (let2 a $ cfg β n (vwk (· + 2) ∘ G))
+  : RWD StepD Γ (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
     (cfg (let2 a β) n G)
   := single $ BCongD.rel $ StepD.cfg_let2_op a β n G
 
 def RWD.cfg_case {Γ : ℕ → ε} (e : Term φ) (r s n G)
   : RWD StepD Γ (cfg (case e r s) n G)
-    (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G))
+    (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
   )
   := single $ BCongD.rel $ StepD.cfg_case e r s n G
 
 def RWD.cfg_case_op {Γ : ℕ → ε} (e : Term φ) (r s n G)
-  : RWD StepD Γ (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
+  : RWD StepD Γ (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
     (cfg (case e r s) n G)
   := single $ BCongD.rel $ StepD.cfg_case_op e r s n G
 
@@ -1218,10 +1239,10 @@ def RWD.let1V0_id {Γ : ℕ → ε} (r : Region φ) (hΓ : Γ 0 = ⊥)
 
 def RWD.let2_eta {Γ : ℕ → ε} (r : Region φ)
   : RWD StepD Γ
-    (let2 (Term.var 0) $
+    (let2 e $
      let1 ((Term.var 1).pair (Term.var 0)) $
-     r.vwk1.vwk1) (let1 (Term.var 0) r)
-  := single $ BCongD.rel $ StepD.let2_eta r
+     r.vwk1.vwk1) (let1 e r)
+  := single $ BCongD.rel $ StepD.let2_eta e r
 
 def RWD.let2_eta_op {Γ : ℕ → ε} (r : Region φ)
   : RWD StepD Γ (let1 (Term.var 0) r)
diff --git a/lake-manifest.json b/lake-manifest.json
index 99488b0..638fcaf 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
+   "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
+   "rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "97a63f4b46b5d410cc6b973bf51519d33110dd9c",
+   "rev": "e446b83b26b1782b8b43647db9f99595678e09b4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/imbrem/discretion.git",
    "type": "git",
    "subDir": null,
-   "rev": "fd860c182549cd06c1944d483dcd519fe6f1c53d",
+   "rev": "c69652d9f40f94ee481926e0582359b0b0116968",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",