diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean
index 4517685d9..575c6a594 100644
--- a/SSA/Projects/PaperExamples/PaperExamples.lean
+++ b/SSA/Projects/PaperExamples/PaperExamples.lean
@@ -35,15 +35,15 @@ instance : OpDenote Op Ty where
     | .const n, _, _ => BitVec.ofInt 32 n
     | .add, .cons (a : BitVec 32) (.cons (b : BitVec 32) .nil), _ => a + b
 
-def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int  :=
-  IExpr.mk
+def cst {Γ : Ctxt _} (n : ℤ) : Expr Op Γ .int  :=
+  Expr.mk
     (op := .const n)
     (ty_eq := rfl)
     (args := .nil)
     (regArgs := .nil)
 
-def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int :=
-  IExpr.mk
+def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr Op Γ .int :=
+  Expr.mk
     (op := .add)
     (ty_eq := rfl)
     (args := .cons e₁ <| .cons e₂ .nil)
@@ -52,28 +52,28 @@ def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int :=
 attribute [local simp] Ctxt.snoc
 
 /-- x + 0 -/
-def lhs : ICom Op (Ctxt.ofList [.int]) .int :=
+def lhs : Com Op (Ctxt.ofList [.int]) .int :=
    -- %c0 = 0
-  ICom.lete (cst 0) <|
+  Com.lete (cst 0) <|
    -- %out = %x + %c0
-  ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <|
+  Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <|
   -- return %out
-  ICom.ret ⟨0, by simp [Ctxt.snoc]⟩
+  Com.ret ⟨0, by simp [Ctxt.snoc]⟩
 
 /-- x -/
-def rhs : ICom Op (Ctxt.ofList [.int]) .int :=
-  ICom.ret ⟨0, by simp⟩
+def rhs : Com Op (Ctxt.ofList [.int]) .int :=
+  Com.ret ⟨0, by simp⟩
 
 def p1 : PeepholeRewrite Op [.int] .int :=
   { lhs := lhs, rhs := rhs, correct :=
     by
       rw [lhs, rhs]
       /-
-      ICom.denote
-        (ICom.lete (cst 0)
-        (ICom.lete (add { val := 1, property := _ } { val := 0, property := _ })
-        (ICom.ret { val := 0, property := ex1.proof_3 }))) =
-      ICom.denote (ICom.ret { val := 0, property := _ })
+      Com.denote
+        (Com.lete (cst 0)
+        (Com.lete (add { val := 1, property := _ } { val := 0, property := _ })
+        (Com.ret { val := 0, property := ex1.proof_3 }))) =
+      Com.denote (Com.ret { val := 0, property := _ })
       -/
       funext Γv
       simp_peephole [add, cst] at Γv
@@ -84,16 +84,16 @@ def p1 : PeepholeRewrite Op [.int] .int :=
       sorry
     }
 
-def ex1' : ICom Op  (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs
+def ex1' : Com Op  (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs
 
 
 theorem EX1' : ex1' = (
   -- %c0 = 0
-  ICom.lete (cst 0) <|
+  Com.lete (cst 0) <|
   -- %out_dead = %x + %c0
-  ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
+  Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
   -- ret %c0
-  ICom.ret ⟨2, by simp [Ctxt.snoc]⟩)
+  Com.ret ⟨2, by simp [Ctxt.snoc]⟩)
   := by rfl
 
 end ToyNoRegion
@@ -132,22 +132,22 @@ instance : OpDenote Op Ty where
       -- let f_k := Nat.iterate f' k
       -- f_k x
 
-def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int  :=
-  IExpr.mk
+def cst {Γ : Ctxt _} (n : ℤ) : Expr Op Γ .int  :=
+  Expr.mk
     (op := .const n)
     (ty_eq := rfl)
     (args := .nil)
     (regArgs := .nil)
 
-def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int :=
-  IExpr.mk
+def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr Op Γ .int :=
+  Expr.mk
     (op := .add)
     (ty_eq := rfl)
     (args := .cons e₁ <| .cons e₂ .nil)
     (regArgs := .nil)
 
-def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : ICom Op [.int] .int) : IExpr Op Γ .int :=
-  IExpr.mk
+def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : Com Op [.int] .int) : Expr Op Γ .int :=
+  Expr.mk
     (op := .iterate k)
     (ty_eq := rfl)
     (args := .cons input .nil)
@@ -156,15 +156,15 @@ def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : ICom Op [.in
 attribute [local simp] Ctxt.snoc
 
 /-- running `f(x) = x + x` 0 times is the identity. -/
-def lhs : ICom Op [.int] .int :=
-  ICom.lete (iterate (k := 0) ⟨0, by simp[Ctxt.snoc]⟩ (
-      ICom.lete (add ⟨0, by simp[Ctxt.snoc]⟩ ⟨0, by simp[Ctxt.snoc]⟩) -- fun x => (x + x)
-      <| ICom.ret ⟨0, by simp[Ctxt.snoc]⟩
+def lhs : Com Op [.int] .int :=
+  Com.lete (iterate (k := 0) ⟨0, by simp[Ctxt.snoc]⟩ (
+      Com.lete (add ⟨0, by simp[Ctxt.snoc]⟩ ⟨0, by simp[Ctxt.snoc]⟩) -- fun x => (x + x)
+      <| Com.ret ⟨0, by simp[Ctxt.snoc]⟩
   )) <|
-  ICom.ret ⟨0, by simp[Ctxt.snoc]⟩
+  Com.ret ⟨0, by simp[Ctxt.snoc]⟩
 
-def rhs : ICom Op [.int] .int :=
-  ICom.ret ⟨0, by simp[Ctxt.snoc]⟩
+def rhs : Com Op [.int] .int :=
+  Com.ret ⟨0, by simp[Ctxt.snoc]⟩
 
 attribute [local simp] Ctxt.snoc
 
@@ -178,14 +178,14 @@ def p1 : PeepholeRewrite Op [.int] .int:=
       rw [lhs, rhs]
       funext Γv
       /-
-      ICom.denote
-        (ICom.lete
+      Com.denote
+        (Com.lete
           (iterate 0 { val := 0, property := lhs.proof_1 }
-            (ICom.lete (add { val := 0, property := lhs.proof_1 } { val := 0, property := lhs.proof_1 })
-              (ICom.ret { val := 0, property := lhs.proof_2 })))
-          (ICom.ret { val := 0, property := lhs.proof_2 }))
+            (Com.lete (add { val := 0, property := lhs.proof_1 } { val := 0, property := lhs.proof_1 })
+              (Com.ret { val := 0, property := lhs.proof_2 })))
+          (Com.ret { val := 0, property := lhs.proof_2 }))
         Γv =
-      ICom.denote (ICom.ret { val := 0, property := rhs.proof_1 }) Γv
+      Com.denote (Com.ret { val := 0, property := rhs.proof_1 }) Γv
       -/
       simp_peephole [add, iterate] at Γv
       /-  ∀ (a : BitVec 32), (fun v => v + v)^[0] a = a -/
@@ -194,15 +194,15 @@ def p1 : PeepholeRewrite Op [.int] .int:=
   }
 
 /-
-def ex1' : ICom Op  (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs
+def ex1' : Com Op  (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs
 
 theorem EX1' : ex1' = (
   -- %c0 = 0
-  ICom.lete (cst 0) <|
+  Com.lete (cst 0) <|
   -- %out_dead = %x + %c0
-  ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
+  Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0
   -- ret %c0
-  ICom.ret ⟨2, by simp [Ctxt.snoc]⟩)
+  Com.ret ⟨2, by simp [Ctxt.snoc]⟩)
   := by rfl
 -/