Term equivalence

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose.lean

@@ -7,11 +7,6 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O
 
 namespace Region
 
-theorem InS.vsubst_ret {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α}
-  (σ : Term.Subst.InS φ (⟨tyIn, ⊥⟩::Γ) _)
-  (t : Term.InS φ (⟨tyIn, ⊥⟩::rest) ⟨tyOut, ⊥⟩)
-  : (InS.ret (targets := targets) t).vsubst σ = InS.ret (t.subst σ) := rfl
-
 abbrev Eqv.ret {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α}
   (t : Term.InS φ (⟨tyIn, ⊥⟩::rest) ⟨tyOut, ⊥⟩)
   : Eqv φ (⟨tyIn, ⊥⟩::rest) (tyOut::targets) := ⟦InS.ret t⟧

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -137,21 +137,27 @@ theorem InS.lwk_congr {Γ : Ctx α ε} {L K : LCtx α} {r r' : InS φ Γ L}
   {ρ ρ' : L.InS K} (hρ : ρ ≈ ρ') (hr : r ≈ r') : r.lwk ρ ≈ r'.lwk ρ'
   := r.lwk_equiv hρ ▸ lwk_congr_right ρ' hr
 
-theorem TStep.vsubst_to_uniform {Γ Δ : Ctx α ε} {L} {r r' : Region φ} {σ : Term.Subst φ}
+theorem TStep.vsubst {Γ Δ : Ctx α ε} {L} {r r' : Region φ} {σ : Term.Subst φ}
   (hσ : σ.Wf Γ Δ) : TStep Δ L r r' → Uniform TStep Γ L (r.vsubst σ) (r'.vsubst σ)
-  | TStep.step d d' p => sorry
+  | TStep.let1_beta de dr => sorry
+  | TStep.rewrite d d' p => sorry
+  | TStep.reduce d d' p => sorry
   | TStep.initial di d d' => sorry
   | TStep.terminal de de' dr => sorry
 
 theorem TStep.vsubst_to_congr {Γ Δ : Ctx α ε} {L}
   {r r' : InS φ Δ L} (σ : Term.Subst.InS φ Γ Δ) (h : TStep Δ L (r : Region φ) (↑r'))
   : r.vsubst σ ≈ r'.vsubst σ := by
   cases r; cases r'
-  exact vsubst_to_uniform σ.prop h
+  exact vsubst σ.prop h
 
 theorem InS.vsubst_congr_right {Γ Δ : Ctx α ε} {L : LCtx α} {r r' : InS φ Δ L}
   (σ : Term.Subst.InS φ Γ Δ) (hr : r ≈ r') : r.vsubst σ ≈ r'.vsubst σ
-  := Uniform.vsubst_flatten TStep.vsubst_to_uniform σ.prop hr
+  := Uniform.vsubst_flatten TStep.vsubst σ.prop hr
+
+-- theorem InS.vsubst_subst_equiv {Γ Δ : Ctx α ε} {L : LCtx α} {r r' : InS φ Δ L}
+--   (σ : Term.Subst.InS φ Γ Δ) (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')
@@ -164,15 +170,15 @@ theorem InS.let1_op {Γ : Ctx α ε} {L : LCtx α}
     : r.let1 (a.op f hf)
     ≈ (r.vwk1.let1 ((Term.InS.var 0 (by simp)).op f hf)).let1 a
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let1_let1 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {r : InS φ (⟨B, ⊥⟩::Γ) L}
   (a : Term.InS φ Γ ⟨A, e⟩) (b : Term.InS φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩)
     : let1 (a.let1 b) r
     ≈ (let1 a $ let1 b $ r.vwk1)
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let1_pair {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
   {r : InS φ (⟨Ty.prod A B, ⊥⟩::Γ) L}
@@ -183,23 +189,23 @@ theorem InS.let1_pair {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
       let1 ((Term.InS.var 1 (by simp)).pair (e := e') (Term.InS.var 0 (by simp))) $
       r.vwk1.vwk1)
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let1_inl {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
   {r : InS φ (⟨A.coprod B, ⊥⟩::Γ) L}
   (a : Term.InS φ Γ ⟨A, e⟩)
     : r.let1 a.inl
     ≈ (r.vwk1.let1 ((Term.InS.var 0 (by simp)).inl (e := e'))).let1 a
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let1_inr {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
   {r : InS φ (⟨A.coprod B, ⊥⟩::Γ) L}
   (b : Term.InS φ Γ ⟨B, e⟩)
     : r.let1 b.inr
     ≈ (r.vwk1.let1 ((Term.InS.var 0 (by simp)).inr (e := e'))).let1 b
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let1_case_t {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {s : InS φ (⟨C, ⊥⟩::Γ) L}
@@ -209,15 +215,15 @@ theorem InS.let1_case_t {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
     : let1 (a.case l r) s
     ≈ case a (let1 l s.vwk1) (let1 r s.vwk1)
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let1_abort {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} (e' := ⊥)
   {r : InS φ (⟨A, ⊥⟩::Γ) L}
   (a : Term.InS φ Γ ⟨Ty.empty, e⟩)
     : r.let1 (a.abort _)
     ≈ (r.vwk1.let1 ((Term.InS.var 0 (by simp)).abort (e := e') _)).let1 a
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let2_op {Γ : Ctx α ε} {L : LCtx α}
   {r : InS φ (⟨C, ⊥⟩::⟨B, ⊥⟩::Γ) L}
@@ -229,7 +235,7 @@ theorem InS.let2_op {Γ : Ctx α ε} {L : LCtx α}
       r.vwk (ρ := ⟨Nat.liftnWk 2 Nat.succ, by apply Ctx.Wkn.sliftn₂; simp⟩))
   := sorry
   -- := Uniform.rel $
-  -- TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  -- TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let2_pair {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {r : InS φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L}
@@ -240,7 +246,7 @@ theorem InS.let2_pair {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
       let1 (b.wk ⟨Nat.succ, (by simp)⟩) r)
   := sorry
   -- := Uniform.rel $
-  -- TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  -- TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let2_abort {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} (e' := ⊥)
   {r : InS φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L}
@@ -251,7 +257,7 @@ theorem InS.let2_abort {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} (e' := ⊥)
       r.vwk ⟨Nat.liftnWk 2 Nat.succ, by apply Ctx.Wkn.sliftn₂; simp⟩)
     := sorry
   -- := Uniform.rel $
-  -- TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  -- TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.case_op {Γ : Ctx α ε} {L : LCtx α}
   (f : φ) (hf : Φ.EFn f A (B.coprod C) e)
@@ -260,15 +266,15 @@ theorem InS.case_op {Γ : Ctx α ε} {L : LCtx α}
     (let1 a $ case (Term.InS.op f hf (Term.InS.var 0 (by simp))) r.vwk1 s.vwk1)
   := sorry
   -- := Uniform.rel $
-  -- TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  -- TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.case_abort {Γ : Ctx α ε} {L : LCtx α} (e' := ⊥)
   (a : Term.InS φ Γ ⟨Ty.empty, e⟩) (r : InS φ (⟨A, ⊥⟩::Γ) L) (s : InS φ (⟨B, ⊥⟩::Γ) L)
   : r.case (a.abort _) s ≈
     (let1 a $ case (Term.InS.abort (e := e') (Term.InS.var 0 (by simp)) (A.coprod B)) r.vwk1 s.vwk1)
   := sorry
   -- := Uniform.rel $
-  -- TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  -- TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 -- TODO: replacements for let1_case, let2_case
 
@@ -280,7 +286,7 @@ theorem InS.cfg_br_lt {Γ : Ctx α ε} {L : LCtx α}
   ≈ (let1 a $ (G ⟨ℓ, hℓ'⟩).vwk_id (by simp only [Ctx.Wkn.lift_id_iff,
     Prod.mk_le_mk, le_refl, and_true, Ctx.Wkn.id]; exact List.get_append ℓ hℓ' ▸ hℓ.get)).cfg R G
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 -- TODO: fix this statement ^
 
@@ -290,15 +296,15 @@ theorem InS.cfg_let1 {Γ : Ctx α ε} {L : LCtx α}
   (G : (i : Fin R.length) → InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
     : (let1 a β).cfg R G ≈ (let1 a $ β.cfg R (λi => (G i).vwk1))
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.cfg_let2 {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.InS φ Γ ⟨Ty.prod A B, ea⟩)
   (R : LCtx α) (β : InS φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (R ++ L))
   (G : (i : Fin R.length) → InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
     : (let2 a β).cfg R G ≈ (let2 a $ β.cfg R (λi => (G i).vwk1.vwk1))
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.cfg_case {Γ : Ctx α ε} {L : LCtx α}
   (e : Term.InS φ Γ ⟨Ty.coprod A B, ea⟩)
@@ -309,7 +315,7 @@ theorem InS.cfg_case {Γ : Ctx α ε} {L : LCtx α}
     : (InS.case e r s).cfg R G
     ≈ InS.case e (r.cfg R (λi => (G i).vwk1)) (s.cfg R (λi => (G i).vwk1))
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.cfg_cfg_eqv_cfg' {Γ : Ctx α ε} {L : LCtx α}
   (R S : LCtx α) (β : InS φ Γ (R ++ (S ++ L)))
@@ -331,7 +337,7 @@ theorem InS.cfg_cfg_eqv_cfg' {Γ : Ctx α ε} {L : LCtx α}
         )
           (by rw [List.append_assoc])))
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by
+  TStep.rewrite InS.coe_wf InS.coe_wf (by
     simp only [Set.mem_setOf_eq, coe_cfg, id_eq, coe_cfg', coe_cast]
     apply Rewrite.cast_trg
     apply Rewrite.cfg_cfg
@@ -347,13 +353,13 @@ theorem InS.cfg_cfg_eqv_cfg' {Γ : Ctx α ε} {L : LCtx α}
       rw [<-hi]
       simp only [Fin.addCases_right]
       rfl
-    ))
+    )
 
 theorem InS.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
   (β : InS φ Γ L)
   : β.cfg [] (λi => i.elim0) ≈ β
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let2_eta {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.InS φ Γ ⟨Ty.prod A B, ea⟩)
@@ -362,7 +368,7 @@ theorem InS.let2_eta {Γ : Ctx α ε} {L : LCtx α}
         let1 ((Term.InS.var 1 ⟨by simp, le_refl _⟩).pair (Term.InS.var 0 (by simp))) r.vwk1.vwk1)
     ≈ let1 a r
   := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor))
+  TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
   (R S : LCtx α) (β : InS φ Γ (R ++ L))
@@ -371,34 +377,27 @@ theorem InS.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
   (hρ : LCtx.Wkn (R ++ L) (S ++ L) (Fin.toNatWk ρ))
   : cfg S (β.lwk ⟨Fin.toNatWk ρ, hρ⟩) (λi => (G i).lwk ⟨Fin.toNatWk ρ, hρ⟩)
   ≈ cfg R β (λi => (G (ρ i)).vwk_id (Ctx.Wkn.id.toFinWk_id hρ i))
-  := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.reduce (by constructor))
+  := Uniform.rel $ TStep.reduce InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.case_inl {Γ : Ctx α ε} {L : LCtx α}
   (e : Term.InS φ Γ ⟨A, ea⟩)
   (r : InS φ (⟨A, ⊥⟩::Γ) L)
   (s : InS φ (⟨B, ⊥⟩::Γ) L)
     : case e.inl r s ≈ let1 e r
-  := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.reduce (by constructor))
+  := Uniform.rel $ TStep.reduce InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.case_inr {Γ : Ctx α ε} {L : LCtx α}
   (e : Term.InS φ Γ ⟨B, ea⟩)
   (r : InS φ (⟨A, ⊥⟩::Γ) L)
   (s : InS φ (⟨B, ⊥⟩::Γ) L)
     : case e.inr r s ≈ let1 e s
-  := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (FStep.reduce (by constructor))
+  := Uniform.rel $ TStep.reduce InS.coe_wf InS.coe_wf (by constructor)
 
 theorem InS.let1_beta {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.InS φ Γ ⟨A, ⊥⟩)
   (r : InS φ (⟨A, ⊥⟩::Γ) L)
     : let1 a r ≈ r.vsubst a.subst0
-  := Uniform.rel $
-  TStep.step InS.coe_wf InS.coe_wf (by
-    constructor
-    sorry
-  )
+  := Uniform.rel $ TStep.let1_beta a.prop r.prop
 
 theorem InS.initial {Γ : Ctx α ε} {L : LCtx α} (hi : Γ.IsInitial) (r r' : InS φ Γ L) : r ≈ r'
   := Uniform.rel (TStep.initial hi r.2 r'.2)

DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean

@@ -123,78 +123,69 @@ structure HaveTrg (Γ : Ctx α ε) (L : LCtx α) (r r' : Region φ) where
 --   | RWD.refl _, d => d
 --   | RWD.cons p s, d => s.wfD (p.wfD d)
 
-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 → 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)
-
--- def TStepD.symm {Γ L} {r r' : Region φ} : TStepD Γ L r r' → TStepD Γ L r' r
---   | step d d' p => step_op d' d p
---   | step_op d d' p => step d' d p
---   | initial i d d' => initial i d' d
---   | terminal e e' d => terminal e' e d
+-- 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 → 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)
 
 inductive TStep : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) → Prop
-  | 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'
+  | let1_beta {e r} : e.Wf Γ ⟨A, ⊥⟩ → r.Wf (⟨A, ⊥⟩::Γ) L
+    → TStep Γ L (let1 e r) (r.vsubst e.subst0)
+  | rewrite {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → Rewrite r r' → TStep Γ L r r'
+  | reduce {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → Reduce 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)
 
--- theorem TStep.symm {Γ L} {r r' : Region φ} : TStep Γ L r r' → TStep Γ L r' r
---   | step d d' p => step_op d' d p
---   | step_op d d' p => step d' d p
---   | initial i d d' => initial i d' d
---   | terminal e e' d => terminal e' e d
-
 theorem TStep.left {Γ L} {r r' : Region φ} : TStep Γ L r r' → r.Wf Γ L
-  | TStep.step d _ _ => d
-  -- | TStep.step_op d _ _ => d
-  | TStep.initial _ d _ => d
-  | TStep.terminal de _ dr => dr.let1 de
+  | let1_beta de dr => dr.let1 de
+  | rewrite d _ _ => d
+  | reduce d _ _ => d
+  | initial _ d _ => d
+  | terminal de _ dr => dr.let1 de
 
 theorem TStep.right {Γ L} {r r' : Region φ} : TStep Γ L r r' → r'.Wf Γ L
-  | TStep.step _ d _ => d
-  -- | TStep.step_op _ d _ => d
-  | TStep.initial _ _ d => d
-  | TStep.terminal _ de dr => dr.let1 de
+  | let1_beta de dr => dr.vsubst de.subst0
+  | rewrite _ d _ => d
+  | reduce _ d _ => d
+  | initial _ _ d => d
+  | terminal _ de dr => dr.let1 de
+
+theorem TStep.cast_src {Γ L} {r₀' r₀ r₁ : Region φ} (h : r₀' = r₀) (p : TStep Γ L r₀ r₁)
+  : TStep Γ L r₀' r₁ := h ▸ p
+
+theorem TStep.cast_trg {Γ L} {r₀ r₁' r₁ : Region φ} (p : TStep Γ L r₀ r₁) (h : r₁ = r₁')
+  : TStep Γ L r₀ r₁' := h ▸ p
 
 theorem TStep.wf {Γ L} {r r' : Region φ} (h : TStep Γ L r r') : r.Wf Γ L ∧ r'.Wf Γ L
-  := ⟨TStep.left h, TStep.right h⟩
+  := ⟨left h, right h⟩
 
 theorem TStep.vwk {Γ Δ : Ctx α ε} {L r r' ρ} (hρ : Γ.Wkn Δ ρ)
   : TStep (φ := φ) Δ L r r' → TStep Γ L (r.vwk ρ) (r'.vwk ρ)
-  | TStep.step d d' p => TStep.step (d.vwk hρ) (d'.vwk hρ)
-    ((p.wk_eff (λi hi => by
-      have hi : i < Δ.length := d.fvs hi
-      have hρ := hρ i hi
-      simp only [Function.comp_apply, Ctx.effect, hρ.length, ↓reduceDIte, List.get_eq_getElem, hi,
-        ge_iff_le]
-      exact hρ.get.2
-      )).vwk ρ)
-  -- | TStep.step_op d d' p => TStep.step_op (d.vwk hρ) (d'.vwk hρ)
-  --   ((p.wk_eff (λi hi => by
-  --     have hi : i < Δ.length := d'.fvs hi
-  --     have hρ := hρ i hi
-  --     simp [Ctx.effect, hρ.length, hi, hρ.get.2]
-  --     )).vwk ρ)
-  | TStep.initial di d d' => TStep.initial (di.wk hρ) (d.vwk hρ) (d'.vwk hρ)
-  | TStep.terminal de de' dr => TStep.terminal (de.wk hρ) (de'.wk hρ) (dr.vwk hρ.slift)
+  | let1_beta de dr => (let1_beta (de.wk hρ) (dr.vwk hρ.slift)).cast_trg
+    (by simp [vsubst_subst0_vwk])
+  | rewrite d d' p => rewrite (d.vwk hρ) (d'.vwk hρ) (p.vwk ρ)
+  | reduce d d' p => reduce (d.vwk hρ) (d'.vwk hρ) (p.vwk ρ)
+  | initial di d d' => initial (di.wk hρ) (d.vwk hρ) (d'.vwk hρ)
+  | terminal de de' dr => terminal (de.wk hρ) (de'.wk hρ) (dr.vwk hρ.slift)
 
 theorem TStep.lwk {Γ : Ctx α ε} {L K r r' ρ} (hρ : L.Wkn K ρ)
   : TStep (φ := φ) Γ L r r' → TStep Γ K (r.lwk ρ) (r'.lwk ρ)
-  | TStep.step d d' p => TStep.step (d.lwk hρ) (d'.lwk hρ) (p.lwk ρ)
-  | TStep.initial di d d' => TStep.initial di (d.lwk hρ) (d'.lwk hρ)
-  | TStep.terminal de de' dr => TStep.terminal de de' (dr.lwk hρ)
+  | let1_beta de dr => (let1_beta de (dr.lwk hρ)).cast_trg (by simp [lwk_vsubst])
+  | rewrite d d' p => rewrite (d.lwk hρ) (d'.lwk hρ) (p.lwk ρ)
+  | reduce d d' p => reduce (d.lwk hρ) (d'.lwk hρ) (p.lwk ρ)
+  | initial di d d' => initial di (d.lwk hρ) (d'.lwk hρ)
+  | terminal de de' dr => terminal de de' (dr.lwk hρ)
 
 -- Note: vsubst needs InS lore for initiality, so that's in Setoid.lean
 
 theorem TStep.lsubst {Γ : Ctx α ε} {L K} {r r' : Region φ} {σ : Subst φ}
   (hσ : σ.Wf Γ L K) : (h : TStep Γ L r r') → TStep Γ K (r.lsubst σ) (r'.lsubst σ)
-  | step d d' p => sorry
+  | let1_beta de dr => (let1_beta de (dr.lsubst hσ.vlift)).cast_trg sorry
+  | rewrite d d' p => sorry--rewrite (d.lsubst hσ) (d'.lsubst hσ) (p.lsubst σ)
+  | reduce d d' p => sorry
   | initial di d d' => initial di (d.lsubst hσ) (d'.lsubst hσ)
   | terminal de de' dr => terminal de de' (dr.lsubst hσ.vlift)