Work towards gloop-ification

imbrem · Sep 22, 2024 · 42c8dd8 · 42c8dd8
1 parent 3e97a01
commit 42c8dd8
Show file tree

Hide file tree

Showing 5 changed files with 171 additions and 28 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean
@@ -406,8 +406,8 @@ theorem Eqv.Pure.central_left {A A' B B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   simp only [Set.mem_setOf_eq, InS.vwk_br, Term.InS.wk_pair, Term.InS.wk_var, Ctx.InS.coe_wk1,
     Nat.liftWk_succ, Nat.succ_eq_add_one, zero_add, Nat.reduceAdd, Nat.liftWk_zero, InS.coe_vsubst,
     Term.InS.coe_subst0, Term.InS.coe_wk, Ctx.InS.coe_wk0, Term.InS.coe_var, InS.coe_vwk,
-    Ctx.InS.coe_wk2, InS.coe_lsubst, InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair, vwk_lsubst,
-    Region.vsubst_lsubst, Term.InS.coe_subst]
+    Ctx.InS.coe_wk2, InS.coe_lsubst, InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair,
+    Region.vwk_lsubst, Region.vsubst_lsubst, Term.InS.coe_subst]
   congr
   · funext k
     cases k with
@@ -519,7 +519,7 @@ theorem Eqv.assoc_left_nat {A B C A' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     Nat.liftWk_zero, Nat.liftWk_succ, Nat.succ_eq_add_one, zero_add, Nat.reduceAdd, InS.coe_vsubst,
     Term.Subst.InS.coe_liftn₂, Term.InS.coe_subst0, Term.InS.coe_var, InS.coe_vwk,
     Ctx.InS.coe_liftn₂, Ctx.InS.coe_wk2, InS.coe_lsubst, InS.coe_alpha0, InS.coe_br,
-    Term.InS.coe_pair, vwk_lsubst, Region.vsubst_lsubst]
+    Term.InS.coe_pair, Region.vwk_lsubst, Region.vsubst_lsubst]
   congr 1
   · funext k; cases k <;> rfl
   · simp only [Region.vwk_vwk]
@@ -569,7 +569,7 @@ theorem Eqv.assoc_mid_nat {A B C B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     Nat.liftWk_zero, Nat.liftWk_succ, Nat.succ_eq_add_one, zero_add, Nat.reduceAdd, InS.coe_vsubst,
     Term.Subst.InS.coe_liftn₂, Term.InS.coe_subst0, Term.InS.coe_var, InS.coe_vwk,
     Ctx.InS.coe_liftn₂, Ctx.InS.coe_wk2, InS.coe_lsubst, InS.coe_alpha0, InS.coe_br,
-    InS.coe_let2, Term.InS.coe_pair, vwk_lsubst, Region.vsubst_lsubst]
+    InS.coe_let2, Term.InS.coe_pair, Region.vwk_lsubst, Region.vsubst_lsubst]
   congr 1
   · funext k; cases k <;> rfl
   · simp only [Region.vwk_vwk]
@@ -596,7 +596,7 @@ theorem Eqv.seq_let2_wk0_pure {Γ : Ctx α ε} {L : LCtx α}
   induction s using Quotient.inductionOn
   apply Eqv.eq_of_reg_eq
   simp only [Set.mem_setOf_eq, InS.coe_vwk, Ctx.InS.coe_lift, Ctx.InS.coe_swap01, InS.coe_lsubst,
-    InS.coe_alpha0, Ctx.InS.coe_wk1, vwk_lsubst, Ctx.InS.coe_swap02]
+    InS.coe_alpha0, Ctx.InS.coe_wk1, Region.vwk_lsubst, Ctx.InS.coe_swap02]
   congr 1
   · funext k
     cases k with
@@ -644,8 +644,8 @@ theorem Eqv.assoc_right_nat {A B C C' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   simp only [Set.mem_setOf_eq, InS.vwk_br, Term.InS.wk_pair, Term.InS.wk_var, Ctx.InS.coe_swap02,
     Nat.ofNat_pos, Nat.swap0_lt, Nat.swap0_0, Nat.one_lt_ofNat, Ctx.InS.coe_wk1, Nat.liftWk_succ,
     Nat.succ_eq_add_one, Nat.reduceAdd, zero_add, Nat.liftWk_zero, InS.coe_vwk, InS.coe_lsubst,
-    InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair, Term.InS.coe_var, vwk_lsubst, InS.coe_vsubst,
-    Term.InS.coe_subst0, Term.Subst.InS.coe_liftn₂, Region.vsubst_lsubst]
+    InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair, Term.InS.coe_var, Region.vwk_lsubst,
+    InS.coe_vsubst, Term.InS.coe_subst0, Term.Subst.InS.coe_liftn₂, Region.vsubst_lsubst]
   congr
   · funext k; cases k with
     | zero => simp

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean
@@ -216,7 +216,7 @@ theorem Eqv.seq_let1_wk0_pure {Γ : Ctx α ε} {L : LCtx α}
   apply Eqv.eq_of_reg_eq
   simp only [Set.mem_setOf_eq, InS.coe_lsubst, InS.coe_alpha0, InS.coe_vwk, Ctx.InS.coe_wk1,
     InS.coe_vsubst, Term.InS.coe_subst0, Term.InS.coe_wk, Ctx.InS.coe_wk0, Ctx.InS.coe_swap01,
-    vwk_lsubst, Region.vsubst_lsubst]
+    Region.vwk_lsubst, Region.vsubst_lsubst]
   congr
   · funext k; cases k with
     | zero =>

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
@@ -444,11 +444,29 @@ theorem Subst.InS.vsubst_congr {Γ Δ : Ctx α ε} {L K : LCtx α}
   (hρ : ρ ≈ ρ') (hσ : σ ≈ σ') : σ.vsubst ρ ≈ σ'.vsubst ρ'
   := λi => Region.InS.vsubst_congr (Term.Subst.InS.slift_congr hρ) (hσ i)
 
--- theorem Eqv.vwk_lsubst {Γ Δ : Ctx α ε}
---   {L K : LCtx α} {σ : Subst.Eqv φ Δ L K} {ρ : Γ.InS Δ}
---   {r : Eqv φ Δ L}
---   : (r.lsubst σ).vwk ρ = (r.vwk ρ).lsubst (σ.vwk ρ)
---   := sorry
+theorem Subst.InS.vwk_congr {Γ Δ : Ctx α ε} {L K : LCtx α}
+  {ρ ρ' : Γ.InS Δ} {σ σ' : Subst.InS φ Δ L K}
+  (hρ : ρ ≈ ρ') (hσ : σ ≈ σ') : σ.vwk ρ ≈ σ'.vwk ρ'
+  := λi => Region.InS.vwk_congr (Ctx.InS.slift_congr hρ) (hσ i)
+
+def Subst.Eqv.vwk {Γ Δ : Ctx α ε} {L K : LCtx α}
+  (ρ : Γ.InS Δ) (σ : Subst.Eqv φ Δ L K) : Subst.Eqv φ Γ L K
+  := Quotient.liftOn σ (λσ => ⟦σ.vwk ρ⟧)
+    (λ_ _ hσ => Quotient.sound <| Subst.InS.vwk_congr (by rfl) hσ)
+
+@[simp]
+theorem Subst.Eqv.vwk_quot {Γ Δ : Ctx α ε} {L K : LCtx α}
+  {ρ : Γ.InS Δ} {σ : Subst.InS φ Δ L K}
+  : vwk ρ ⟦σ⟧ = ⟦σ.vwk ρ⟧ := rfl
+
+theorem Eqv.vwk_lsubst {Γ Δ : Ctx α ε}
+  {L K : LCtx α} {σ : Subst.Eqv φ Δ L K} {ρ : Γ.InS Δ}
+  {r : Eqv φ Δ L}
+  : (r.lsubst σ).vwk ρ = (r.vwk ρ).lsubst (σ.vwk ρ)
+  := by
+  induction r using Quotient.inductionOn
+  induction σ using Quotient.inductionOn
+  simp [InS.vwk_lsubst]
 
 def Subst.Eqv.vsubst {Γ Δ : Ctx α ε} {L K : LCtx α}
   (ρ : Term.Subst.Eqv φ Γ Δ) (σ : Subst.Eqv φ Δ L K) : Subst.Eqv φ Γ L K
@@ -694,6 +712,11 @@ theorem Subst.Eqv.fromFCFG_quot {Γ : Ctx α ε} {L K : LCtx α}
   : fromFCFG (λi => ⟦G i⟧) = ⟦Region.CFG.toSubst G⟧ := by
   simp [fromFCFG, Quotient.finChoice_eq_choice]
 
+theorem Subst.Eqv.get_fromFCFG {Γ : Ctx α ε} {L K : LCtx α}
+  {G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) K} {i : Fin L.length}
+  : (fromFCFG G).get i = G i
+  := by induction G using Eqv.choiceInduction; rw [Subst.Eqv.fromFCFG_quot]; simp
+
 def Subst.Eqv.fromFCFG_append {Γ : Ctx α ε} {L K R : LCtx α}
   (G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) (K ++ R))
   : Subst.Eqv φ Γ (L ++ R) (K ++ R)

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
@@ -237,24 +237,23 @@ theorem Eqv.cfg_unpack_rec {Γ : Ctx α ε} {R L : LCtx α}
   · rw [Subst.Eqv.vlift_extend, Subst.Eqv.vlift_unpack]
   · rw [Subst.Eqv.unpack_zero]
 
--- theorem Eqv.gloop_pack_entry_rec {Γ : Ctx α ε} {R L : LCtx α}
---   {β : Eqv φ Γ (R ++ L)} {G : Eqv φ (⟨R.pack, ⊥⟩::Γ) (R.pack::L)}
---   : gloop R.pack (β.lsubst Subst.Eqv.pack.extend) G
---   = cfg R β (λi => (ret (Term.Eqv.inj_n R i) ;; G).lsubst Subst.Eqv.unpack.extend)
---   := sorry
-
 theorem Eqv.packed_out_cfg_liftn {Γ : Ctx α ε} {R L : LCtx α}
   {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
   : (cfg R β G).packed_out
   = cfg R (β.lsubst (Subst.Eqv.pack.liftn_append _))
           (λi => (G i).lsubst (Subst.Eqv.pack.liftn_append _))
   := by simp only [packed_out, lsubst_cfg, Subst.Eqv.vlift_liftn_append, Subst.Eqv.vlift_pack]
 
-theorem Eqv.lsubst_pack_append_unpack {Γ : Ctx α ε} {L R : LCtx α}
-  : lsubst (Subst.Eqv.liftn_append R Subst.Eqv.pack).vlift (unpack (φ := φ) (Γ := Γ) (R := R ++ L))
-  = case (Term.Eqv.pack_app (e := ⊥))
+def Eqv.unpack_right_out {Γ : Ctx α ε} {R L : LCtx α}
+  : Eqv φ (((R ++ L).pack, ⊥)::Γ) (R ++ [L.pack]) :=
+  case (Term.Eqv.pack_app (e := ⊥))
     (br (List.length R) Term.Eqv.nil (by simp))
-    (lwk_id LCtx.Wkn.id_right_append unpack) := by
+    (lwk_id LCtx.Wkn.id_right_append unpack)
+
+theorem Eqv.lsubst_pack_append_vlift_unpack {Γ : Ctx α ε} {L R : LCtx α}
+  : lsubst (Subst.Eqv.liftn_append R Subst.Eqv.pack).vlift (unpack (φ := φ) (Γ := Γ) (R := R ++ L))
+  = unpack_right_out := by
+  rw [unpack_right_out]
   induction R with
   | nil => simp only [List.nil_append, Subst.Eqv.liftn_append_empty, Subst.Eqv.vlift_pack,
     lsubst_pack_unpack, LCtx.pack.eq_1, Term.Eqv.pack_app, Term.Eqv.inj_l, List.length_nil,
@@ -308,15 +307,114 @@ theorem Eqv.lsubst_pack_append_unpack {Γ : Ctx α ε} {L R : LCtx α}
       apply eq_of_reg_eq
       simp
 
+theorem Eqv.lsubst_pack_append_unpack {Γ : Ctx α ε} {L R : LCtx α}
+  : lsubst (Subst.Eqv.liftn_append R Subst.Eqv.pack) (unpack (φ := φ) (Γ := Γ) (R := R ++ L))
+  = unpack_right_out := by
+  convert lsubst_pack_append_vlift_unpack
+  rw [Subst.Eqv.vlift_liftn_append, Subst.Eqv.vlift_pack]
+
+def Subst.Eqv.unpack_right_out {Γ : Ctx α ε} {R L : LCtx α}
+  : Subst.Eqv φ Γ [(R ++ L).pack] (R ++ [L.pack]) := (Eqv.case (Term.Eqv.pack_app (e := ⊥))
+    (Eqv.br R.length Term.Eqv.nil (by simp))
+    (Region.Eqv.unpack.lwk_id LCtx.Wkn.id_right_append)).csubst
+
+def Eqv.unpacked_right_out {Γ : Ctx α ε} {R L : LCtx α} (β : Eqv φ Γ [(R ++ L).pack])
+  : Eqv φ Γ (R ++ [L.pack]) := β.lsubst Subst.Eqv.unpack_right_out
 
 theorem Eqv.unpacked_out_pack_liftn {Γ : Ctx α ε} {R L : LCtx α}
   {β : Eqv φ Γ [(R ++ L).pack]}
   : β.unpacked_out.lsubst (Subst.Eqv.pack.liftn_append R)
-  = β.lsubst (case (Term.Eqv.pack_app (e := ⊥))
-    (br R.length Term.Eqv.nil (by simp))
-    (unpack.lwk_id LCtx.Wkn.id_right_append)).csubst := by
+  = β.unpacked_right_out := by
   rw [unpacked_out, lsubst_lsubst]; congr; ext k; cases k using Fin.elim1
-  simp [Subst.Eqv.get_comp, Subst.Eqv.unpack_zero, lsubst_pack_append_unpack]
+  simp [
+    Subst.Eqv.get_comp, Subst.Eqv.unpack_zero, Subst.Eqv.unpack_right_out,
+    lsubst_pack_append_vlift_unpack, unpack_right_out,
+  ]
+
+theorem Eqv.packed_out_cfg_unpacked_out {Γ : Ctx α ε} {R L : LCtx α}
+  {β : Eqv φ Γ [(R ++ L).pack]} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) [(R ++ L).pack]}
+  : (cfg R β.unpacked_out (λi => (G i).unpacked_out)).packed_out
+  = (cfg R β.unpacked_right_out (λi => (G i).unpacked_right_out))
+  := by simp [packed_out, unpacked_out_pack_liftn, Subst.Eqv.vlift_liftn_append]
+
+theorem Eqv.packed_out_cfg {Γ : Ctx α ε} {R L : LCtx α}
+  {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : (cfg R β G).packed_out
+  = (cfg R β.packed_out.unpacked_right_out (λi => (G i).packed_out.unpacked_right_out)) := calc
+  _ = (cfg R β.packed_out.unpacked_out (λi => (G i).packed_out.unpacked_out)).packed_out := by simp
+  _ = _ := by rw [packed_out_cfg_unpacked_out]
+
+def Eqv.unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
+  : Eqv φ (((R ++ L).pack, ⊥)::Γ) [R.pack, L.pack] :=
+  case (Term.Eqv.pack_app (e := ⊥))
+    (br 1 Term.Eqv.nil (by simp))
+    (nil)
+
+@[simp]
+theorem Eqv.vwk1_unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
+  : (unpack_app_out (φ := φ) (Γ := Γ) (R := R) (L := L)).vwk1 (inserted := inserted)
+  = unpack_app_out := by simp only [unpack_app_out, vwk1_case, Term.Eqv.wk1_pack_app]; rfl
+
+def Subst.Eqv.unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
+  : Subst.Eqv φ Γ [(R ++ L).pack] [R.pack, L.pack] := Region.Eqv.unpack_app_out.csubst
+
+@[simp]
+theorem Subst.Eqv.vlift_unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
+  : (Subst.Eqv.unpack_app_out (φ := φ) (Γ := Γ) (R := R) (L := L)).vlift (head := head)
+  = unpack_app_out := by
+  ext k; cases k using Fin.elim1
+  simp [unpack_app_out]
+
+theorem Subst.Eqv.extend_unpack_comp_unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
+  : Subst.Eqv.unpack.extend.comp Subst.Eqv.unpack_app_out
+  = Subst.Eqv.unpack_right_out (φ := φ) (Γ := Γ) (R := R) (L := L) := by
+  ext k; cases k using Fin.elim1
+  simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero,
+    List.getElem_cons_zero, List.singleton_append, unpack_app_out, Region.Eqv.unpack_app_out,
+    get_comp, Eqv.csubst_get, Eqv.cast_rfl, Eqv.lsubst_case, Eqv.lsubst_br, List.length_cons,
+    Nat.reduceAdd, Fin.mk_one, Fin.val_one, List.getElem_cons_succ, get_vlift, Eqv.vwk_id_eq,
+    unpack_right_out]
+  congr
+  · simp only [unpack_def, extend_quot, List.singleton_append, get_quot, List.get_eq_getElem,
+    List.length_cons, List.length_singleton, Nat.reduceAdd, Fin.val_one, List.getElem_cons_succ,
+    List.getElem_cons_zero, Eqv.vwk1_quot]
+    apply Region.Eqv.eq_of_reg_eq
+    simp
+  · simp only [unpack_def, extend_quot, List.singleton_append, vlift_quot, Eqv.lsubst_quot,
+    Region.Eqv.unpack_def, Region.InS.unpack, Set.mem_setOf_eq, Eqv.lwk_id_quot]
+    apply Region.Eqv.eq_of_reg_eq
+    simp only [Set.mem_setOf_eq, InS.coe_lsubst, lsubst, Term.InS.coe_var, InS.coe_vlift,
+      Subst.vlift, InS.coe_extend, InS.coe_unpack, List.length_singleton, Function.comp_apply,
+      Subst.extend, zero_lt_one, ↓reduceIte, csubst, InS.coe_lwk_id, Region.vsubst0_var0_vwk1]
+    rw [Region.vwk1_unpack]
+
+def Eqv.unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α} (r : Eqv φ Γ [(R ++ L).pack])
+  : Eqv φ Γ [R.pack, L.pack] := r.lsubst Subst.Eqv.unpack_app_out
+
+theorem Eqv.vwk1_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ (V::Γ) [(R ++ L).pack]}
+  : r.unpacked_app_out.vwk1 (inserted := inserted) = r.vwk1.unpacked_app_out := by rw [
+    unpacked_app_out, <-Subst.Eqv.vlift_unpack_app_out, Subst.Eqv.vwk1_lsubst_vlift,
+    Subst.Eqv.vlift_unpack_app_out, Subst.Eqv.vlift_unpack_app_out, <-unpacked_app_out]
+
+theorem Eqv.extend_unpack_unpacked_app_out
+  {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ Γ [(R ++ L).pack]}
+  : r.unpacked_app_out.lsubst Subst.Eqv.unpack.extend = r.unpacked_right_out := by
+  rw [unpacked_app_out, lsubst_lsubst, Subst.Eqv.extend_unpack_comp_unpack_app_out]; rfl
+
+theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α}
+  {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : (cfg R β G).packed_out
+  = gloop R.pack β.packed_out.unpacked_app_out
+      (unpack.lsubst (Subst.Eqv.fromFCFG (λi => (G i).vwk1.packed_out.unpacked_app_out))) := calc
+  _ = (cfg R (β.packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend)
+              (λi => (G i).packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend.vlift))
+      := by simp [packed_out_cfg, extend_unpack_unpacked_app_out, Subst.Eqv.vlift_extend]
+  _ = _ := by
+    rw [dinaturality_to_gloop_rec]
+    congr
+    · ext k; simp [Subst.Eqv.get_fromFCFG]
+      sorry
+    · simp [Subst.Eqv.unpack]
 
 end Region
 

diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
@@ -516,6 +516,23 @@ theorem Region.InS.lsubst_lsubst {Γ : Ctx α ε}
   : (r.lsubst τ).lsubst σ = r.lsubst (σ.comp τ)
   := by ext; simp [Region.lsubst_lsubst]
 
+def Region.Subst.InS.vwk {Γ Δ : Ctx α ε}
+  (ρ : Γ.InS Δ) (σ : Region.Subst.InS φ Δ L K)
+  : Region.Subst.InS φ Γ L K
+  := ⟨Region.vwk (Nat.liftWk ρ.val) ∘ σ.val, (λi => (σ.prop i).vwk ρ.prop.slift)⟩
+
+@[simp]
+theorem Region.Subst.InS.coe_vwk {Γ Δ : Ctx α ε}
+  (ρ : Γ.InS Δ) (σ : Region.Subst.InS φ Δ L K)
+  : (σ.vwk ρ : Region.Subst φ) = Region.vwk (Nat.liftWk ρ.val) ∘ (σ : Region.Subst φ)
+  := rfl
+
+@[simp]
+theorem Region.Subst.InS.get_vwk {Γ Δ : Ctx α ε}
+  {ρ : Γ.InS Δ} {σ : Region.Subst.InS φ Δ L K} {i : Fin L.length}
+  : (σ.vwk ρ).get i = (σ.get i).vwk ρ.slift
+  := rfl
+
 def Region.Subst.InS.vsubst {Γ Δ : Ctx α ε}
   (ρ : Term.Subst.InS φ Γ Δ) (σ : Region.Subst.InS φ Δ L K)
   : Region.Subst.InS φ Γ L K
@@ -544,6 +561,11 @@ theorem Region.Subst.InS.vsubst_comp {Γ Δ Ξ : Ctx α ε}
 
 -- TODO: vsubst_comp, and other lore...
 
+theorem Region.InS.vwk_lsubst {Γ Δ : Ctx α ε}
+  {ρ : Γ.InS Δ} {σ : Region.Subst.InS φ Δ L K} {r : Region.InS φ Δ L}
+  : (r.lsubst σ).vwk ρ = (r.vwk ρ).lsubst (σ.vwk ρ)
+  := by ext; simp [Region.vwk_lsubst]
+
 theorem Region.InS.vsubst_lsubst {Γ Δ : Ctx α ε}
   {σ : Region.Subst.InS φ Δ L K} {ρ : Term.Subst.InS φ Γ Δ}
   {r : Region.InS φ Δ L}
@@ -643,7 +665,7 @@ theorem Region.InS.vwk1_lsubst_vlift {Γ : Ctx α ε} {L K : LCtx α}
   : (r.lsubst σ.vlift).vwk1 (inserted := inserted) = r.vwk1.lsubst σ.vlift.vlift := by
   ext
   simp only [Set.mem_setOf_eq, vwk1, coe_vwk, Ctx.InS.coe_wk1, coe_lsubst, Subst.InS.coe_vlift,
-    Subst.vlift, vwk_lsubst]
+    Subst.vlift, Region.vwk_lsubst]
   congr
   simp only [<-Function.comp.assoc, Region.vwk1, <-Region.vwk_comp]
   apply congrFun