Removed wk_cfg, dead_cfg rules

imbrem · Sep 11, 2024 · 8d97638 · 8d97638
1 parent eb88475
commit 8d97638
Show file tree

Hide file tree

Showing 5 changed files with 141 additions and 139 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
@@ -1221,20 +1221,20 @@ theorem Eqv.choiceInduction {ι : Type _} {Γs : ι → Ctx α ε} {Ls : ι →
     simp only [hG]
     apply choice
 
-theorem Eqv.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
-  (R S : LCtx α) (β : Eqv φ Γ (R ++ L))
-  (G : (i : Fin S.length) → Eqv φ ((List.get S i, ⊥)::Γ) (R ++ L))
-  (ρ : Fin R.length → Fin S.length)
-  (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))
-  := by
-  induction β using Quotient.inductionOn
-  induction G using Eqv.choiceInduction
-  simp only [cfg, Set.mem_setOf_eq, lwk_quot, List.get_eq_getElem, Fin.getElem_fin, vwk_id_quot,
-    Quotient.finChoice_eq, Eqv.cfg_inner_quot]
-  apply Eqv.sound
-  apply InS.wk_cfg
+-- theorem Eqv.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
+--   (R S : LCtx α) (β : Eqv φ Γ (R ++ L))
+--   (G : (i : Fin S.length) → Eqv φ ((List.get S i, ⊥)::Γ) (R ++ L))
+--   (ρ : Fin R.length → Fin S.length)
+--   (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))
+--   := by
+--   induction β using Quotient.inductionOn
+--   induction G using Eqv.choiceInduction
+--   simp only [cfg, Set.mem_setOf_eq, lwk_quot, List.get_eq_getElem, Fin.getElem_fin, vwk_id_quot,
+--     Quotient.finChoice_eq, Eqv.cfg_inner_quot]
+--   apply Eqv.sound
+--   apply InS.wk_cfg
 
 theorem Eqv.let1_let1_case {Γ : Ctx α ε}
   {a : Term.Eqv φ Γ ⟨Ty.coprod A B, e⟩}

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
@@ -399,14 +399,14 @@ theorem InS.let2_eta {Γ : Ctx α ε} {L : LCtx α}
 
 -- TODO: case_eta
 
-theorem InS.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
-  (R S : LCtx α) (β : InS φ Γ (R ++ L))
-  (G : (i : Fin S.length) → InS φ ((List.get S i, ⊥)::Γ) (R ++ L))
-  (ρ : Fin R.length → Fin S.length)
-  (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.reduce InS.coe_wf InS.coe_wf (by constructor)
+-- theorem InS.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
+--   (R S : LCtx α) (β : InS φ Γ (R ++ L))
+--   (G : (i : Fin S.length) → InS φ ((List.get S i, ⊥)::Γ) (R ++ L))
+--   (ρ : Fin R.length → Fin S.length)
+--   (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.reduce InS.coe_wf InS.coe_wf (by constructor)
 
 -- theorem InS.dead_cfg_left {Γ : Ctx α ε} {L : LCtx α}
 --   (R S : LCtx α) (β : InS φ Γ (S ++ L))

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean
@@ -164,11 +164,11 @@ def RWD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n)
     (cfg β k (G ∘ ρ))
   := single $ BCongD.rel $ StepD.wk_cfg β n G k ρ
 
-def RWD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G')
-  : RWD StepD Γ
-    (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
-    (cfg β m G')
-  := single $ BCongD.rel $ StepD.dead_cfg_left β n G m G'
+-- def RWD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G')
+--   : RWD StepD Γ
+--     (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
+--     (cfg β m G')
+--   := single $ BCongD.rel $ StepD.dead_cfg_left β n G m G'
 
 def RWD.swap_cfg' {Γ : ℕ → ε} (β : Region φ) (n G m G')
   : RWD StepD Γ
@@ -341,25 +341,25 @@ def RWD.cfg_blocks {P} {Γ : ℕ → ε} (β n) (G G' : Fin n → Region φ)
   : RWD P Γ (Region.cfg β n G) (Region.cfg β n G')
   := cast_trg (cfg_blocks_partial β n G G' h n) (by simp)
 
-def RWD.dead_cfg_right {Γ : ℕ → ε} (β : Region φ) (n G m G')
-  : RWD StepD Γ
-    (cfg (β.lwk (n.liftnWk (· + m))) (n + m) (Fin.addCases (lwk (n.liftnWk (· + m)) ∘ G) G'))
-    (cfg β n G) :=
-    (cast_trg (swap_cfg (β.lwk (n.liftnWk (· + m))) n (lwk (n.liftnWk (· + m)) ∘ G) m G')
-      (by rw [
-        Fin.comp_addCases, lwk_lwk, <-Function.comp.assoc, comp_lwk,
-        Fin.toNatWk_swapAdd_comp_liftnWk_add]
-      )).comp
-    (dead_cfg_left β m _ n G)
-
-def RWD.cfg_elim {Γ : ℕ → ε} (β : Region φ) (n G)
-  : RWD StepD Γ (cfg (β.lwk (· + n)) n G) β
-  :=
-  let s : RWD StepD Γ
-    (cfg (β.lwk (· + n)) n G)
-    (cfg (β.lwk (· + n)) (n + 0) (Fin.addCases G (lwk (· + n) ∘ Fin.elim0)))
-    := RWD.of_eq (by simp [Fin.addCases_zero])
-  (s.comp (dead_cfg_left β n G 0 Fin.elim0)).comp (RWD.cfg_zero _ _)
+-- def RWD.dead_cfg_right {Γ : ℕ → ε} (β : Region φ) (n G m G')
+--   : RWD StepD Γ
+--     (cfg (β.lwk (n.liftnWk (· + m))) (n + m) (Fin.addCases (lwk (n.liftnWk (· + m)) ∘ G) G'))
+--     (cfg β n G) :=
+--     (cast_trg (swap_cfg (β.lwk (n.liftnWk (· + m))) n (lwk (n.liftnWk (· + m)) ∘ G) m G')
+--       (by rw [
+--         Fin.comp_addCases, lwk_lwk, <-Function.comp.assoc, comp_lwk,
+--         Fin.toNatWk_swapAdd_comp_liftnWk_add]
+--       )).comp
+--     (dead_cfg_left β m _ n G)
+
+-- def RWD.cfg_elim {Γ : ℕ → ε} (β : Region φ) (n G)
+--   : RWD StepD Γ (cfg (β.lwk (· + n)) n G) β
+--   :=
+--   let s : RWD StepD Γ
+--     (cfg (β.lwk (· + n)) n G)
+--     (cfg (β.lwk (· + n)) (n + 0) (Fin.addCases G (lwk (· + n) ∘ Fin.elim0)))
+--     := RWD.of_eq (by simp [Fin.addCases_zero])
+--   (s.comp (dead_cfg_left β n G 0 Fin.elim0)).comp (RWD.cfg_zero _ _)
   -- := match β with
   -- | Region.br ℓ e => (cfg_br_ge (ℓ + n) e n G (by simp)).cast_trg (by simp)
   -- | Region.let1 a β => (cfg_let1 a (β.lwk (· + n)) n G).comp (let1 a (cfg_elim β n _))

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean
@@ -38,14 +38,14 @@ open Term
 inductive ReduceD : Region φ → Region φ → Type _
   | case_inl (e r s) : ReduceD (case (inl e) r s) (let1 e r)
   | case_inr (e r s) : ReduceD (case (inr e) r s) (let1 e s)
-  | wk_cfg (β n G k) (ρ : Fin k → Fin n) :
-    ReduceD
-      (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
-      (cfg β k (G ∘ ρ))
-  | dead_cfg_left (β n G m G') :
-    ReduceD
-      (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
-      (cfg β m G')
+  -- | wk_cfg (β n G k) (ρ : Fin k → Fin n) :
+  --   ReduceD
+  --     (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
+  --     (cfg β k (G ∘ ρ))
+  -- | dead_cfg_left (β n G m G') :
+  --   ReduceD
+  --     (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
+  --     (cfg β m G')
   | ucfg' (β n G) : ReduceD (cfg β n G) (ucfg' n β G)
   -- | codiagonal (β G : Region φ) :
   --   ReduceD
@@ -55,14 +55,14 @@ inductive ReduceD : Region φ → Region φ → Type _
 inductive Reduce : Region φ → Region φ → Prop
   | case_inl (e r s) : Reduce (case (inl e) r s) (let1 e r)
   | case_inr (e r s) : Reduce (case (inr e) r s) (let1 e s)
-  | wk_cfg (β n G k) (ρ : Fin k → Fin n) :
-    Reduce
-      (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
-      (cfg β k (G ∘ ρ))
-  | dead_cfg_left (β n G m G') :
-    Reduce
-      (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
-      (cfg β m G')
+  -- | wk_cfg (β n G k) (ρ : Fin k → Fin n) :
+  --   Reduce
+  --     (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
+  --     (cfg β k (G ∘ ρ))
+  -- | dead_cfg_left (β n G m G') :
+  --   Reduce
+  --     (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
+  --     (cfg β m G')
   | ucfg' (β n G) : Reduce (cfg β n G) (ucfg' n β G)
   -- | codiagonal (β G : Region φ) :
   --   Reduce
@@ -114,18 +114,19 @@ def ReduceD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (d : ReduceD r r')
   : 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]
+  -- | 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]
   | ucfg' β n G =>
     convert ucfg' (β.vsubst σ) n (λi => (G i).vsubst σ.lift)
     simp only [Region.ucfg', vsubst_lsubst]
@@ -152,61 +153,62 @@ def ReduceD.lsubst {r r' : Region φ} (σ : Subst φ) (d : ReduceD r r')
   : 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]
+  -- | 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]
   | ucfg' β n G =>
     convert ucfg' (β.lsubst (σ.liftn n)) n (λi => (G i).lsubst (σ.liftn n).vlift)
     simp only [Region.ucfg', lsubst_lsubst]

diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean
@@ -150,17 +150,17 @@ def StepD.case_inr {Γ : ℕ → ε} (e : Term φ) (r s)
   : StepD Γ (case (inr e) r s) (let1 e s)
   := StepD.reduce (ReduceD.case_inr e r s)
 
-@[match_pattern]
-def StepD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n)
-  : StepD Γ (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
-    (cfg β k (G ∘ ρ))
-  := StepD.reduce (ReduceD.wk_cfg β n G k ρ)
+-- @[match_pattern]
+-- def StepD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n)
+--   : StepD Γ (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
+--     (cfg β k (G ∘ ρ))
+--   := StepD.reduce (ReduceD.wk_cfg β n G k ρ)
 
-@[match_pattern]
-def StepD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G')
-  : StepD Γ (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
-    (cfg β m G')
-  := StepD.reduce (ReduceD.dead_cfg_left β n G m G')
+-- @[match_pattern]
+-- def StepD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G')
+--   : StepD Γ (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
+--     (cfg β m G')
+--   := StepD.reduce (ReduceD.dead_cfg_left β n G m G')
 
 @[match_pattern]
 def StepD.let1_op {Γ : ℕ → ε} (f e) (r : Region φ)