lsubst/vsubst for reduction and rewriting of region

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean

@@ -440,11 +440,11 @@ theorem Eqv.fixpoint_dinaturality_seq_cfg {A B C : Ty α} {Γ : Ctx α ε} {L :
 --             (Fin.elim1 (f.lwk1 ;; (inj_l.coprod g.lwk1 ;; left_exit)).vwk1) := by
 --   sorry
 
-theorem Eqv.fixpoint_dinaturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod C)::L))
-  (g : Eqv φ (⟨C, ⊥⟩::Γ) ((B.coprod A)::L))
-  : fixpoint (f ;; coprod inj_l g) = f ;; coprod nil (fixpoint (g ;; coprod inj_l f))
-  := by sorry
+-- theorem Eqv.fixpoint_dinaturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+--   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod C)::L))
+--   (g : Eqv φ (⟨C, ⊥⟩::Γ) ((B.coprod A)::L))
+--   : fixpoint (f ;; coprod inj_l g) = f ;; coprod nil (fixpoint (g ;; coprod inj_l f))
+--   := by sorry
 
 end Region
 

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -549,36 +549,36 @@ def Subst.Eqv.fromFCFG_append {Γ : Ctx α ε} {L K R : LCtx α}
   : Subst.Eqv φ Γ (L ++ R) (K ++ R)
   := Quotient.liftOn (Quotient.finChoice G) (λG => ⟦Region.CFG.toSubst_append G⟧) sorry
 
-theorem Eqv.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
-  {σ : Subst.Eqv φ Γ R (R' ++ L)} {β : Eqv φ Γ (R ++ L)}
-  {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (R ++ L)}
-  : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
-  = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG_append G).vlift)
-  := by
-  induction σ using Quotient.inductionOn
-  induction β using Quotient.inductionOn
-  sorry
-
-theorem Eqv.dinaturality_from_one {Γ : Ctx α ε} {R L : LCtx α}
-  {σ : Subst.Eqv φ Γ R (B::L)} {β : Eqv φ Γ (R ++ L)}
-  {G : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ L)}
-  : cfg [B] (β.lsubst σ.extend_in) (Fin.elim1 $ G.lsubst σ.extend_in.vlift)
-  = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG_append (L := [B]) (Fin.elim1 G)).vlift)
-  := dinaturality (Γ := Γ) (R := R) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
-
-theorem Eqv.dinaturality_to_one {Γ : Ctx α ε} {R' L : LCtx α}
-  {σ : Subst.Eqv φ Γ [A] (R' ++ L)} {β : Eqv φ Γ (A::L)}
-  {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (A::L)}
-  : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
-  = cfg [A] β (Fin.elim1 $ (σ.get _).lsubst (Subst.Eqv.fromFCFG_append G).vlift)
-  := dinaturality (Γ := Γ) (R := [A]) (R' := R') (L := L) (σ := σ) (β := β) (G := G)
-
-theorem Eqv.dinaturality_one {Γ : Ctx α ε} {L : LCtx α}
-  {σ : Subst.Eqv φ Γ [A] ([B] ++ L)} {β : Eqv φ Γ (A::L)}
-  {G : Eqv φ (⟨B, ⊥⟩::Γ) ([A] ++ L)}
-  : cfg [B] (β.lsubst σ.extend_in) (Fin.elim1 $ G.lsubst σ.extend_in.vlift)
-  = cfg [A] β (Fin.elim1 $ (σ.get _).lsubst (Subst.Eqv.fromFCFG_append (Fin.elim1 G)).vlift)
-  := dinaturality (Γ := Γ) (R := [A]) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
+-- theorem Eqv.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
+--   {σ : Subst.Eqv φ Γ R (R' ++ L)} {β : Eqv φ Γ (R ++ L)}
+--   {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (R ++ L)}
+--   : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
+--   = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG_append G).vlift)
+--   := by
+--   induction σ using Quotient.inductionOn
+--   induction β using Quotient.inductionOn
+--   sorry
+
+-- theorem Eqv.dinaturality_from_one {Γ : Ctx α ε} {R L : LCtx α}
+--   {σ : Subst.Eqv φ Γ R (B::L)} {β : Eqv φ Γ (R ++ L)}
+--   {G : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ L)}
+--   : cfg [B] (β.lsubst σ.extend_in) (Fin.elim1 $ G.lsubst σ.extend_in.vlift)
+--   = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG_append (L := [B]) (Fin.elim1 G)).vlift)
+--   := dinaturality (Γ := Γ) (R := R) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
+
+-- theorem Eqv.dinaturality_to_one {Γ : Ctx α ε} {R' L : LCtx α}
+--   {σ : Subst.Eqv φ Γ [A] (R' ++ L)} {β : Eqv φ Γ (A::L)}
+--   {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (A::L)}
+--   : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
+--   = cfg [A] β (Fin.elim1 $ (σ.get _).lsubst (Subst.Eqv.fromFCFG_append G).vlift)
+--   := dinaturality (Γ := Γ) (R := [A]) (R' := R') (L := L) (σ := σ) (β := β) (G := G)
+
+-- theorem Eqv.dinaturality_one {Γ : Ctx α ε} {L : LCtx α}
+--   {σ : Subst.Eqv φ Γ [A] ([B] ++ L)} {β : Eqv φ Γ (A::L)}
+--   {G : Eqv φ (⟨B, ⊥⟩::Γ) ([A] ++ L)}
+--   : cfg [B] (β.lsubst σ.extend_in) (Fin.elim1 $ G.lsubst σ.extend_in.vlift)
+--   = cfg [A] β (Fin.elim1 $ (σ.get _).lsubst (Subst.Eqv.fromFCFG_append (Fin.elim1 G)).vlift)
+--   := dinaturality (Γ := Γ) (R := [A]) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
 
 def Subst.InS.initial {Γ : Ctx α ε} {L : LCtx α}
   : Subst.InS φ Γ [] L := ⟨Subst.id, λi => i.elim0⟩

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -179,10 +179,6 @@ theorem InS.vsubst_congr_right {Γ Δ : Ctx α ε} {L : LCtx α}
   (σ : Term.Subst.InS φ Γ Δ) {r r' : InS φ Δ L} (hr : r ≈ r') : r.vsubst σ ≈ r'.vsubst σ
   := Uniform.vsubst_flatten TStep.vsubst σ.prop hr
 
--- theorem InS.vsubst_congr {Γ Δ : Ctx α ε} {L r r' : InS φ Δ L}
---   {σ σ' : Term.Subst.InS φ Γ Δ} (hσ : σ ≈ σ') (hr : r ≈ r')
---   : r.vsubst σ ≈ r'.vsubst σ' := sorry
-
 open Term.InS
 
 theorem InS.let1_op {Γ : Ctx α ε} {L : LCtx α}
@@ -635,10 +631,10 @@ theorem InS.codiagonal {Γ : Ctx α ε} {L : LCtx α}
     funext i; cases i using Fin.elim1
     rfl
 
-theorem InS.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
-  {σ : Subst.InS φ Γ R (R' ++ L)} {β : InS φ Γ (R ++ L)}
-  {G : (i : Fin R'.length) → InS φ (⟨R'.get i, ⊥⟩::Γ) (R ++ L)}
-  : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
-  ≈ cfg R β (λi => (σ.cfg i).lsubst (CFG.toSubst_append G).vlift) := by
-  rw [eqv_def]
-  convert Uniform.dinaturality σ.prop β.prop (λi => (G i).prop)
+-- theorem InS.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
+--   {σ : Subst.InS φ Γ R (R' ++ L)} {β : InS φ Γ (R ++ L)}
+--   {G : (i : Fin R'.length) → InS φ (⟨R'.get i, ⊥⟩::Γ) (R ++ L)}
+--   : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
+--   ≈ cfg R β (λi => (σ.cfg i).lsubst (CFG.toSubst_append G).vlift) := by
+--   rw [eqv_def]
+--   convert Uniform.dinaturality σ.prop β.prop (λi => (G i).prop)

DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean

@@ -57,17 +57,17 @@ inductive Uniform (P : Ctx α ε → LCtx α → Region φ → Region φ → Pro
       → β.Wf Γ (R ++ L)
       → (∀i : Fin n, (G i).Wf ((R.get (i.cast hR.symm), ⊥)::Γ) (R ++ L)) →
       Uniform P Γ L (cfg β n G) (ucfg' n β G)
-  | dinaturality {Γ : Ctx α ε} {L R R' : LCtx α} {β : Region φ}
-    {G : Fin R'.length → Region φ} {σ : Subst φ}
-    : σ.Wf Γ R (R' ++ L)
-      → β.Wf Γ (R ++ L)
-      → (∀i : Fin R'.length, (G i).Wf ((R'.get i, ⊥)::Γ) (R ++ L))
-      → Uniform P Γ L
-        (cfg
-          (β.lsubst (σ.extend R.length R'.length)) R'.length
-          (λi => (G i).lsubst (σ.extend R.length R'.length).vlift))
-        (cfg β R.length
-          (λi => (σ i).lsubst (Subst.fromFCFG R.length G).vlift))
+  -- | dinaturality {Γ : Ctx α ε} {L R R' : LCtx α} {β : Region φ}
+  --   {G : Fin R'.length → Region φ} {σ : Subst φ}
+  --   : σ.Wf Γ R (R' ++ L)
+  --     → β.Wf Γ (R ++ L)
+  --     → (∀i : Fin R'.length, (G i).Wf ((R'.get i, ⊥)::Γ) (R ++ L))
+  --     → Uniform P Γ L
+  --       (cfg
+  --         (β.lsubst (σ.extend R.length R'.length)) R'.length
+  --         (λi => (G i).lsubst (σ.extend R.length R'.length).vlift))
+  --       (cfg β R.length
+  --         (λi => (σ i).lsubst (Subst.fromFCFG R.length G).vlift))
   | refl : r.Wf Γ L → Uniform P Γ L r r
   | rel : P Γ L x y → Uniform P Γ L x y
   | symm : Uniform P Γ L x y → Uniform P Γ L y x
@@ -153,9 +153,9 @@ theorem Uniform.wf {P : Ctx α ε → LCtx α → Region φ → Region φ → Pr
       intro i; cases i using Fin.elim1;
       apply dG.lsubst Wf.nil.lsubst0
   | ucfg hR dβ dG => exact ⟨Wf.cfg _ _ hR dβ dG, Wf.ucfg' _ _ hR dβ dG⟩
-  | dinaturality hσ dβ dG => exact ⟨
-      Wf.cfg _ _ rfl (dβ.lsubst hσ.extend_in) (λi => (dG i).lsubst hσ.extend_in.vlift),
-      Wf.cfg _ _ rfl dβ (λi => (hσ i).lsubst (Subst.Wf.fromFCFG_append dG).vlift)⟩
+  -- | dinaturality hσ dβ dG => exact ⟨
+  --     Wf.cfg _ _ rfl (dβ.lsubst hσ.extend_in) (λi => (dG i).lsubst hσ.extend_in.vlift),
+  --     Wf.cfg _ _ rfl dβ (λi => (hσ i).lsubst (Subst.Wf.fromFCFG_append dG).vlift)⟩
   | refl h => exact ⟨h, h⟩
   | rel h => exact toWf h
   | symm _ I => exact I.symm
@@ -250,13 +250,13 @@ theorem Uniform.vwk {P Q : Ctx α ε → LCtx α → Region φ → Region φ →
   | ucfg hR dβ dG =>
     simp only [vwk_cfg, vwk_ucfg']
     exact ucfg hR (dβ.vwk hρ) (λi => (dG i).vwk hρ.slift)
-  | dinaturality hσ dβ dG =>
-    rename_i L R R' β G σ
-    rw [vwk_dinaturality_left, vwk_dinaturality_right]
-    exact dinaturality
-      (σ := (Region.vwk (Nat.liftWk ρ)) ∘ σ)
-      (λi => (hσ i).vwk hρ.slift) (dβ.vwk hρ)
-      (λi => (dG i).vwk hρ.slift)
+  -- | dinaturality hσ dβ dG =>
+  --   rename_i L R R' β G σ
+  --   rw [vwk_dinaturality_left, vwk_dinaturality_right]
+  --   exact dinaturality
+  --     (σ := (Region.vwk (Nat.liftWk ρ)) ∘ σ)
+  --     (λi => (hσ i).vwk hρ.slift) (dβ.vwk hρ)
+  --     (λi => (dG i).vwk hρ.slift)
 
 theorem Uniform.lwk {P Q : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L K r r'}
   (toLwk : ∀{Γ L K ρ r r'}, L.Wkn K ρ → P Γ L r r' → Q Γ K (r.lwk ρ) (r'.lwk ρ))
@@ -308,8 +308,15 @@ theorem Uniform.lwk {P Q : Ctx α ε → LCtx α → Region φ → Region φ →
   | ucfg hR dβ dG =>
     simp only [lwk_cfg, lwk_ucfg']
     exact ucfg hR (dβ.lwk (hR ▸ hρ.liftn_append)) (λi => (dG i).lwk (hR ▸ hρ.liftn_append))
-  | dinaturality hσ hβ hG =>
-    sorry
+  -- | dinaturality hσ hβ hG =>
+  --   rename_i L R R' β G σ
+  --   convert dinaturality
+  --     (σ := (Region.lwk (Nat.liftnWk R'.length ρ)) ∘ σ)
+  --     (λi => sorry)
+  --     (hβ.lwk (hρ.liftn_append _))
+  --     (λi => (hG i).lwk (hρ.liftn_append _)) using 1
+  --   · sorry
+  --   · sorry
 
 theorem Uniform.vsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ Δ L r r'}
   (toVsubst : ∀{Γ Δ L σ r r'}, σ.Wf Γ Δ → P Δ L r r' → Q Γ L (r.vsubst σ) (r'.vsubst σ))
@@ -341,13 +348,22 @@ theorem Uniform.vsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
       exact Ih
   | codiagonal hβ hG =>
     convert (codiagonal (hβ.vsubst hσ) (hG.vsubst hσ.slift)) using 1
-    · sorry
-    · sorry
+    · simp only [BinSyntax.Region.vsubst, cfg.injEq, heq_eq_eq, true_and]
+      funext i; cases i using Fin.elim1
+      simp only [BinSyntax.Region.vsubst, subst, Subst.lift_zero, nil, ret, Fin.isValue,
+        Fin.elim1_zero, cfg.injEq, heq_eq_eq, true_and]
+      funext i; cases i using Fin.elim1
+      simp [vsubst_lift₂_vwk1]
+    · simp only [BinSyntax.Region.vsubst, cfg.injEq, heq_eq_eq, true_and]
+      funext i; cases i using Fin.elim1
+      simp only [Fin.isValue, Fin.elim1_zero, vsubst_lsubst]
+      congr
+      funext i; cases i <;> rfl
   | ucfg hR dβ dG =>
     simp only [vsubst_cfg, vsubst_ucfg']
     exact ucfg hR (dβ.vsubst hσ) (λi => (dG i).vsubst hσ.slift)
-  | dinaturality hσ hβ hG =>
-    sorry
+  -- | dinaturality hσ hβ hG =>
+  --   sorry
 
 theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L K r r'}
   (toLsubst : ∀{Γ L K σ r r'}, σ.Wf Γ L K → P Γ L r r' → Q Γ K (r.lsubst σ) (r'.lsubst σ))
@@ -384,14 +400,33 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
       exact Ih
   | codiagonal hβ hG =>
     convert codiagonal (hβ.lsubst hσ.slift) (hG.lsubst hσ.vlift.slift.slift) using 1
-    · sorry
-    · sorry
+    · simp only [BinSyntax.Region.lsubst, Subst.liftn_one, cfg.injEq, heq_eq_eq, true_and]
+      funext i
+      cases i using Fin.elim1
+      simp [nil, ret]
+      funext i
+      cases i using Fin.elim1
+      simp only [Subst.liftn_one, ← Subst.vlift_lift_comm, Fin.isValue, Fin.elim1_zero, vwk1_lsubst]
+      simp [Subst.vlift, <-Function.comp.assoc, vwk2_comp_vwk1]
+    · simp only [BinSyntax.Region.lsubst, Subst.liftn_one, cfg.injEq, heq_eq_eq, true_and]
+      funext i
+      cases i using Fin.elim1
+      simp only [Fin.isValue, Fin.elim1_zero, lsubst_lsubst]
+      congr
+      funext k; cases k using Nat.cases2 with
+      | rest k =>
+        simp only [Subst.comp, BinSyntax.Region.lsubst, Subst.vlift, Function.comp_apply,
+          Subst.lift, vsubst0_var0_vwk1, lwk_lwk]
+        simp only [vwk1_lwk]
+        simp only [← lsubst_fromLwk, lsubst_lsubst]
+        rfl
+      | _ => rfl
   | ucfg hR dβ dG =>
     simp only [lsubst_cfg, lsubst_ucfg']
     exact ucfg hR (dβ.lsubst (hσ.liftn_append' hR.symm))
       (λi => (dG i).lsubst (hσ.liftn_append' hR.symm).vlift)
-  | dinaturality hσ hβ hG =>
-    sorry
+  -- | dinaturality hσ hβ hG =>
+  --   sorry
 
 theorem Uniform.vsubst_flatten {P : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ Δ L r r'}
   (toVsubst : ∀{Γ Δ L σ r r'}, σ.Wf Γ Δ → P Δ L r r' → Uniform P Γ L (r.vsubst σ) (r'.vsubst σ))

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean

@@ -150,16 +150,85 @@ theorem Reduce.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Red
   := let ⟨d⟩ := p.nonempty; (d.lwk ρ).reduce
 
 def ReduceD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (d : ReduceD r r')
-  : ReduceD (r.vsubst σ) (r'.vsubst σ)
-  := sorry
+  : ReduceD (r.vsubst σ) (r'.vsubst σ) := by cases d with
+  | case_inl e r s => exact case_inl (e.subst σ) (r.vsubst σ.lift) (s.vsubst σ.lift)
+  | case_inr e r s => exact case_inr (e.subst σ) (r.vsubst σ.lift) (s.vsubst σ.lift)
+  | wk_cfg β n G k ρ =>
+    convert wk_cfg (β.vsubst σ) n (λi => (G i).vsubst σ.lift) k ρ
+    simp only [BinSyntax.Region.vsubst, vsubst_lwk, Function.comp_apply, cfg.injEq, heq_eq_eq,
+      true_and]
+    rfl
+  | dead_cfg_left β n G m G' =>
+    convert dead_cfg_left (β.vsubst σ) n (λi => (G i).vsubst σ.lift) m (λi => (G' i).vsubst σ.lift)
+    simp only [BinSyntax.Region.vsubst, vsubst_lwk, Function.comp_apply, cfg.injEq, heq_eq_eq,
+      true_and]
+    funext i
+    simp only [Fin.addCases, Function.comp_apply, eq_rec_constant]
+    split <;> simp [vsubst_lwk]
 
 theorem Reduce.vsubst
   {r r' : Region φ} (σ : Term.Subst φ) (p : Reduce r r') : Reduce (r.vsubst σ) (r'.vsubst σ)
   := let ⟨d⟩ := p.nonempty; (d.vsubst σ).reduce
 
 def ReduceD.lsubst {r r' : Region φ} (σ : Subst φ) (d : ReduceD r r')
-  : ReduceD (r.lsubst σ) (r'.lsubst σ)
-  := sorry
+  : ReduceD (r.lsubst σ) (r'.lsubst σ) := by cases d with
+  | case_inl e r s => exact case_inl e (r.lsubst σ.vlift) (s.lsubst σ.vlift)
+  | case_inr e r s => exact case_inr e (r.lsubst σ.vlift) (s.lsubst σ.vlift)
+  | wk_cfg β n G k ρ =>
+    convert wk_cfg (β.lsubst (σ.liftn k)) n (λi => (G i).lsubst (σ.liftn k).vlift) k ρ
+    simp only [
+      BinSyntax.Region.lsubst, lsubst_lwk, Function.comp_apply, cfg.injEq, heq_eq_eq, true_and]
+    constructor
+    · rw [<-lsubst_fromLwk, lsubst_lsubst]; congr
+      funext i
+      simp only [Function.comp_apply, Subst.liftn, Fin.toNatWk, Subst.comp, Subst.fromLwk_vlift]
+      split
+      · simp [Fin.toNatWk, *]
+      · simp only [add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right,
+        lsubst_fromLwk, lwk_lwk]
+        congr; funext i
+        simp [Fin.toNatWk]
+    · funext i
+      simp only [← lsubst_fromLwk, Function.comp_apply, lsubst_lsubst]; congr
+      funext i
+      simp only [Function.comp_apply, Subst.liftn, Fin.toNatWk, Subst.comp, Subst.fromLwk_vlift]
+      split
+      · simp [Subst.vlift, Subst.liftn, vwk1, Fin.toNatWk, *]
+      · simp only [Subst.vlift, Function.comp_apply, Subst.liftn, add_lt_iff_neg_right,
+        not_lt_zero', ↓reduceIte, add_tsub_cancel_right, vwk1_lwk, *]
+        simp only [← lsubst_fromLwk, lsubst_lsubst]
+        congr
+        funext i; simp [Subst.comp, Fin.toNatWk]
+  | dead_cfg_left β n G m G' =>
+    convert dead_cfg_left (β.lsubst (σ.liftn m)) n (λi => (G i).lsubst (σ.liftn (n + m)).vlift) m
+      (λi => (G' i).lsubst (σ.liftn m).vlift)
+    simp only [
+      BinSyntax.Region.lsubst, lsubst_lwk, Function.comp_apply, cfg.injEq, heq_eq_eq, true_and]
+    constructor
+    · simp only [←lsubst_fromLwk, lsubst_lsubst]
+      congr
+      funext i; simp_arith only [Function.comp_apply, Subst.liftn, Subst.comp, Subst.fromLwk_vlift]
+      split; rfl
+      simp only [lsubst_fromLwk, lwk_lwk, comp_add_right]
+      congr 2
+      funext i; omega
+      rw [Nat.add_comm n m, Nat.add_sub_add_right]
+    · funext i
+      simp only [Fin.addCases, Function.comp_apply, eq_rec_constant]
+      split; rfl
+      simp only [<-lsubst_fromLwk, lsubst_lsubst]
+      congr
+      funext i
+      simp_arith only [
+        Subst.comp, BinSyntax.Region.lsubst, Subst.vlift, Function.comp_apply, Subst.liftn,
+        Subst.vwk1_comp_fromLwk
+      ]
+      split
+      · rfl
+      · simp only [vsubst0_var0_vwk1, lsubst_fromLwk, ← vwk1_lwk, lwk_lwk, comp_add_right]
+        congr 3
+        funext i; omega
+        rw [Nat.add_comm n m, Nat.add_sub_add_right]
 
 theorem Reduce.lsubst
   {r r' : Region φ} (σ : Subst φ) (p : Reduce r r') : Reduce (r.lsubst σ) (r'.lsubst σ)