diff --git a/LeanSubst/List.lean b/Archive/List.lean
similarity index 100%
rename from LeanSubst/List.lean
rename to Archive/List.lean
diff --git a/Examples/LambdaCalc.lean b/Examples/LambdaCalc.lean
index 0209aba..ba7de64 100644
--- a/Examples/LambdaCalc.lean
+++ b/Examples/LambdaCalc.lean
@@ -11,7 +11,7 @@ namespace LeanSubst.Examples.LambdaCalc
   infixl:65 " :@ " => Term.app
 
   @[coe]
-  def Term.from_action : Subst.Action Term -> Term
+  def Term.from_action : Action Term -> Term
   | re y => var y
   | su t => t
 
@@ -29,34 +29,34 @@ namespace LeanSubst.Examples.LambdaCalc
   @[simp, grind =]
   theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action]
 
-  instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where
+  instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where
     coe := Term.from_action
 
   @[simp]
-  def rmap (r : Ren) : Term -> Term
+  def rmap (r : Ren Term) : Term -> Term
   | .var x => .var (r.act x)
   | t1 :@ t2 => rmap r t1 :@ rmap r t2
   | :λ t => :λ rmap r.lift t
 
-  instance : RenMap Term where
+  instance : RenMap Term Term where
     rmap := rmap
 
   @[simp, grind =]
-  theorem ren_var {x} {r : Ren} : (Term.var x)⟨r⟩ = .var (r.act x) := by
+  theorem ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by
     simp [RenMap.rmap]
 
   @[simp, grind =]
-  theorem ren_app {t1 t2} {r : Ren} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
+  theorem ren_app {t1 t2} {r : Ren Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
     simp [RenMap.rmap]
 
   @[simp, grind =]
-  theorem ren_lam {t} {r : Ren} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
+  theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
     simp [RenMap.rmap]
 
-  instance : RenMapId Term where
+  instance : RenMapId Term Term where
     apply_id := by subst_solve_id
 
-  instance : RenMapCompose Term where
+  instance : RenMapCompose Term Term where
     apply_compose := by subst_solve_compose
 
   @[simp]
@@ -88,16 +88,24 @@ namespace LeanSubst.Examples.LambdaCalc
     generalize zdef : σ.act x = z
     cases z <;> simp [Term.from_action]
 
+  @[simp]
+  theorem Term.from_action_compose_ren {x} {σ : Subst Term} {r : Ren Term}
+    : (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x)
+  := by
+    simp [Term.from_action]
+    generalize zdef : σ.act x = z
+    cases z <;> simp
+
   instance : SubstMapId Term Term where
     apply_id := by subst_solve_id
 
-  instance : SubstMapStable Term where
+  instance : SubstMapStable Term Term where
     apply_stable := by subst_solve_stable
 
   instance : SubstMapRenComposeLeft Term Term where
     apply_ren_compose_left := by subst_solve_compose
 
-  instance : SubstMapRenComposeRight Term Term where
+  instance : SubstMapRenComposeRight Term where
     apply_ren_compose_right := by subst_solve_compose
 
   instance : SubstMapCompose Term Term where
diff --git a/Examples/LambdaCalcKit.lean b/Examples/LambdaCalcKit.lean
index 3f75821..8b89f00 100644
--- a/Examples/LambdaCalcKit.lean
+++ b/Examples/LambdaCalcKit.lean
@@ -11,7 +11,7 @@ namespace LeanSubst.Examples.LambdaCalc
   infixl:65 " :@ " => Term.app
 
   @[coe]
-  def Term.from_action : Subst.Action Term -> Term
+  def Term.from_action : Action Term -> Term
   | re y => var y
   | su t => t
 
@@ -29,11 +29,11 @@ namespace LeanSubst.Examples.LambdaCalc
   @[simp, grind =]
   theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action]
 
-  instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where
+  instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where
     coe := Term.from_action
 
   @[simp]
-  def Term.ren_act (r : Ren) : Term -> Term
+  def Term.ren_act (r : Ren Term) : Term -> Term
   | .var x => .var (r.act x)
   | t => t
 
@@ -47,12 +47,12 @@ namespace LeanSubst.Examples.LambdaCalc
     lift (f : A) (k : Nat := 1) : A
 
   @[simp]
-  instance : Kit Term Ren where
+  instance : Kit Term (Ren Term) where
     act := Term.ren_act
     lift f n := Ren.lift f n
 
   @[simp]
-  instance [RenMap Term] : Kit Term (Subst Term) where
+  instance [RenMap Term Term] : Kit Term (Subst Term) where
     act := Term.subst_act
     lift f n := Subst.lift f n
 
@@ -63,27 +63,27 @@ namespace LeanSubst.Examples.LambdaCalc
   | :λ t => :λ kitmap (kit.lift σ) t
 
   @[simp]
-  def rmap (r : Ren) : Term -> Term := kitmap r
+  def rmap (r : Ren Term) : Term -> Term := kitmap r
 
-  instance : RenMap Term where
+  instance : RenMap Term Term where
     rmap := rmap
 
   @[simp, grind =]
-  theorem ren_var {x} {r : Ren} : (Term.var x)⟨r⟩ = .var (r.act x) := by
+  theorem ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by
     simp +instances [RenMap.rmap]
 
   @[simp, grind =]
-  theorem ren_app {t1 t2} {r : Ren} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
+  theorem ren_app {t1 t2} {r : Ren Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
     simp [RenMap.rmap]
 
   @[simp, grind =]
-  theorem ren_lam {t} {r : Ren} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
+  theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
     simp +instances [RenMap.rmap]
 
-  instance : RenMapId Term where
+  instance : RenMapId Term Term where
     apply_id := by intro t; induction t <;> simp [*]
 
-  instance : RenMapCompose Term where
+  instance : RenMapCompose Term Term where
     apply_compose := by subst_solve_compose
 
   @[simp]
@@ -112,16 +112,24 @@ namespace LeanSubst.Examples.LambdaCalc
     generalize zdef : σ.act x = z
     cases z <;> simp [Term.from_action]
 
+  @[simp]
+  theorem Term.from_action_compose_ren {x} {σ : Subst Term} {r : Ren Term}
+    : (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x)
+  := by
+    simp [Term.from_action]
+    generalize zdef : σ.act x = z
+    cases z <;> simp
+
   instance : SubstMapId Term Term where
     apply_id := by subst_solve_id
 
-  instance : SubstMapStable Term where
+  instance : SubstMapStable Term Term where
     apply_stable := by subst_solve_stable
 
   instance : SubstMapRenComposeLeft Term Term where
     apply_ren_compose_left := by subst_solve_compose
 
-  instance : SubstMapRenComposeRight Term Term where
+  instance : SubstMapRenComposeRight Term where
     apply_ren_compose_right := by subst_solve_compose
 
   instance : SubstMapCompose Term Term where
diff --git a/LeanSubst.lean b/LeanSubst.lean
index 0d966e3..e5654ba 100644
--- a/LeanSubst.lean
+++ b/LeanSubst.lean
@@ -1,9 +1,8 @@
 
-import LeanSubst.Ren
-import LeanSubst.HetRen
-import LeanSubst.Subst
+import LeanSubst.Basic
+import LeanSubst.Ops
 import LeanSubst.Laws
-import LeanSubst.Option
-import LeanSubst.List
-import LeanSubst.Reduction
-import LeanSubst.Normal
+import LeanSubst.Types.Option
+import LeanSubst.Types.List
+import LeanSubst.Rewriting.Reduction
+import LeanSubst.Rewriting.Normal
diff --git a/LeanSubst/Basic.lean b/LeanSubst/Basic.lean
new file mode 100644
index 0000000..e058419
--- /dev/null
+++ b/LeanSubst/Basic.lean
@@ -0,0 +1,44 @@
+
+namespace LeanSubst
+
+universe u1 u2
+variable {S : Type u1} {T : Type u2}
+
+structure Ren (T : Type u2) where
+  act : Nat -> Nat
+
+class RenMap (S : Type u1) (T : Type u2) where
+  rmap : Ren T -> S -> S
+
+export RenMap (rmap)
+
+macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t)
+
+@[app_unexpander rmap]
+def unexpand_rmap : Lean.PrettyPrinter.Unexpander
+| `($_ $r $t) => `($t⟨$r⟩)
+| _ => throw ()
+
+inductive Action (T : Type u2) where
+| re : Nat -> Action T
+| su : T -> Action T
+deriving Repr
+
+export Action (re su)
+
+structure Subst (T : Type u2) where
+  act : Nat -> Action T
+
+class SubstMap (S : Type u1) (T : Type u2) where
+  smap : Subst T -> S -> S
+
+export SubstMap (smap)
+
+macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t)
+
+@[app_unexpander smap]
+def unexpand_smap : Lean.PrettyPrinter.Unexpander
+| `($_ $σ $t) => `($t[$σ])
+| _ => throw ()
+
+end LeanSubst
diff --git a/LeanSubst/HetRen.lean b/LeanSubst/HetRen.lean
deleted file mode 100644
index 40fa887..0000000
--- a/LeanSubst/HetRen.lean
+++ /dev/null
@@ -1,123 +0,0 @@
-import LeanSubst.Ren
-
-namespace LeanSubst
-  universe u
-  variable {S T : Type}
-
-  structure HetRen (T : Type) where
-    act : Nat -> Nat
-
-  def HetRen.id T : HetRen T := ⟨λ x => x⟩
-
-  def HetRen.add T (k : Nat) : HetRen T := ⟨(· + k)⟩
-
-  def HetRen.sub T (k : Nat) : HetRen T := ⟨(· - k)⟩
-
-  def HetRen.lift (r : HetRen T) (k : Nat := 1) : HetRen T := .mk λ n =>
-    if n < k then n else r.act (n - k) + k
-
-  def HetRen.cons (a : Nat) (r : HetRen T) : HetRen T := .mk λ n =>
-    match n with
-    | 0 => a
-    | n + 1 => r.act n
-
-  def HetRen.append : List Nat -> HetRen T -> HetRen T
-  | .nil, r => r
-  | .cons hd tl, r => append tl (r.cons hd)
-
-  instance : HAppend (List Nat) (HetRen T) (HetRen T) where
-    hAppend := HetRen.append
-
-  def HetRen.compose : HetRen T -> HetRen T -> HetRen T
-  | r1, r2 => .mk λ n => r2.act (r1.act n)
-
-  def Ren.het T (r : Ren) : HetRen T := ⟨r.act⟩
-
-  @[simp]
-  theorem Ren.het_action {T i} {r : Ren} : (r.het T).act i = r.act i := by simp [Ren.het]
-
-  class HetRenMap (S T : Type) where
-    hrmap : HetRen T -> S -> S
-
-  export HetRenMap (hrmap)
-
-  macro:max t:term noWs "⟨" r:term "⟩" : term => `(hrmap $r $t)
-  infixr:67 (name := HetRen.cons_notation) " :: " => HetRen.cons
-  infixr:85 (name := HetRen.compose_notation) " ∘ " => HetRen.compose
-
-  @[app_unexpander hrmap]
-  def unexpandHetRenApply : Lean.PrettyPrinter.Unexpander
-  | `($_ $r $t) => `($t⟨$r⟩)
-  | _ => throw ()
-
-  @[simp, grind =]
-  theorem HetRen.lift_zero {r : HetRen T} : r.lift 0 = r := by
-    unfold HetRen.lift; congr
-
-  @[grind =]
-  theorem HetRen.lift_succ {r : HetRen T} {k} : r.lift (k + 1) = (r.lift k).lift := by
-    induction k; simp
-    case _ n ih =>
-      unfold HetRen.lift; congr; funext; case _ i =>
-      simp; unfold HetRen.lift at ih; simp at ih
-      grind
-
-  @[simp]
-  theorem HetRen.id_action {x} : (HetRen.id T).act x = x := by simp [HetRen.id]
-
-  @[simp]
-  theorem HetRen.lift_id {k} : HetRen.lift (HetRen.id T) k = HetRen.id T := by
-    simp [HetRen.id, HetRen.lift]; congr; funext; case _ x =>
-    cases x <;> simp; omega
-
-  @[simp]
-  theorem HetRen.cons_head_action {n} {r : HetRen T} : (n::r).act 0 = n := by simp [HetRen.cons]
-
-  @[simp]
-  theorem HetRen.cons_tail_action {n i} {r : HetRen T} : (n::r).act (i + 1) = r.act i := by simp [HetRen.cons]
-
-  @[simp]
-  theorem HetRen.compose_id_left {r : HetRen T} : (id T) ∘ r = r := by
-    simp [HetRen.compose, HetRen.id]
-
-  @[simp]
-  theorem HetRen.compose_id_right {r : HetRen T} : r ∘ (id T) = r := by
-    simp [HetRen.compose, HetRen.id]
-
-  @[simp]
-  theorem HetRen.compose_assoc {r1 r2 r3 : HetRen T} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by
-    simp [HetRen.compose]
-
-  @[simp]
-  theorem HetRen.compose_action {r1 r2 : HetRen T} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by
-    simp [HetRen.compose]
-
-  theorem HetRen.compose_lift_k1 {r1 r2 : HetRen T} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by
-    simp [HetRen.compose, HetRen.lift]
-    funext; case _ x =>
-    cases x <;> simp
-
-  @[simp]
-  theorem HetRen.compose_lift {k} {r1 r2 : HetRen T} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by
-    induction k generalizing r1 r2; simp
-    case _ k ih =>
-      rw [lift_succ, ih]
-      rw [lift_succ (r := r1)]
-      rw [lift_succ (r := r2)]
-      rw [compose_lift_k1]
-
-  class HetRenMapId (S T : Type) [HetRenMap S T] where
-    apply_id {t : S} : t⟨HetRen.id T⟩ = t
-
-  class HetRenMapCompose (S T : Type) [HetRenMap S T] where
-    apply_compose {s : S} {r1 r2 : HetRen T} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩
-
-  @[simp, grind =]
-  theorem HetRen.apply_id [HetRenMap S T] [HetRenMapId S T] {t : S} : t⟨id T⟩ = t := HetRenMapId.apply_id
-
-  @[simp, grind =]
-  theorem HetRen.apply_compose [HetRenMap S T] [HetRenMapCompose S T] {t : S} {r1 r2 : HetRen T}
-    : t⟨r1⟩⟨r2⟩ = t⟨r1 ∘ r2⟩
-  := HetRenMapCompose.apply_compose
-
-end LeanSubst
diff --git a/LeanSubst/Laws.lean b/LeanSubst/Laws.lean
index 2c87803..7d51b02 100644
--- a/LeanSubst/Laws.lean
+++ b/LeanSubst/Laws.lean
@@ -1,566 +1,409 @@
-import LeanSubst.Ren
-import LeanSubst.Subst
+
+import LeanSubst.Basic
+import LeanSubst.Ops
 
 namespace LeanSubst
-  universe u
-  variable {S T : Type}
-
-  class SubstMapId (S T : Type) [RenMap T] [SubstMap S T] where
-    apply_id {t : S} : t[+0:T] = t
-
-  class SubstMapStable (S : Type) [RenMap S] [SubstMap S S] where
-    apply_stable (r : Ren) (σ : Subst S) : r = σ -> rmap (T := S) r = smap σ
-
-  class SubstMapRenCommute (S T : Type) [RenMap S] [RenMap T] [SubstMap S T] where
-    apply_ren_commute {s : S} (r : Ren) (τ : Subst T) : s⟨r⟩[τ:T] = s[τ:T]⟨r⟩
-
-  class SubstMapRenComposeLeft (S T : Type) [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] where
-    apply_ren_compose_left {s : S} {r : Ren} {τ : Subst T} : s[r.to:T][τ:_] = s[r.to ∘ τ:T]
-
-  class SubstMapRenComposeRight (S T : Type) [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] where
-    apply_ren_compose_right {s : S} {r : Ren} {σ : Subst T} : s[σ:_][r.to:T] = s[σ ∘ r.to:T]
-
-  class SubstMapCompose (S T : Type) [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] where
-    apply_compose {s : S} {σ τ : Subst T} : s[σ:T][τ:_] = s[σ ∘ τ:T]
-
-  class SubstMapHetCompose (S T : Type) [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] where
-    apply_hcompose {s : S} {σ : Subst S} {τ : Subst T} : s[σ][τ:T] = s[τ:T][σ ◾ τ]
-
-  namespace Subst
-    export SubstMapStable (apply_stable)
-    export SubstMapRenCommute (apply_ren_commute)
-    export SubstMapRenComposeLeft (apply_ren_compose_left)
-    export SubstMapRenComposeRight (apply_ren_compose_right)
-  end Subst
-
-  theorem Ren.lift_eq_from_eq [RenMap T] [SubstMap S T] {r : Ren} {σ : Subst T}
-    : r = σ -> r.lift = σ.lift
-  := by intro h; rw [<-h, to_lift]
-
-  namespace Subst
-    section
-      @[simp, grind =]
-      theorem rewrite1 : re 0 :: +1 = +0@T := by
-        simp [Subst.cons, Subst.id]
-        funext; case _ x =>
-        cases x; all_goals simp
-
-      open SubstMap
-      variable [RenMap T]
-
-      @[simp, grind =]
-      theorem I_lift {k} : +0.lift k = +0@T := by
-        funext; case _ x =>
-        cases x; all_goals (simp [Subst.lift, Subst.id])
-        grind
-
-      @[simp, grind =]
-      theorem rewrite2 [SubstMap T T] {σ : Subst T} : +0 ∘ σ = σ := by
-        funext; case _ x =>
-        unfold Subst.compose; simp [Subst.id]
-
-      @[simp, grind =]
-      theorem rewrite3_replace [SubstMap T T] {σ τ : Subst T} {s : T}
-        : (su s :: σ) ∘ τ = su s[τ] :: (σ ∘ τ)
-      := by
-        simp [Subst.cons, Subst.compose]
-        funext; case _ x =>
-        cases x; all_goals simp
-
-      @[simp, grind =]
-      theorem rewrite3_rename [SubstMap T T] {s} {σ τ : Subst T}
-        : (re s :: σ) ∘ τ = (τ.act s) :: (σ ∘ τ)
-      := by
-        simp [Subst.cons, Subst.compose]
-        funext; case _ x =>
-        cases x; all_goals simp
-
-      @[simp, grind =]
-      theorem rewrite4 [SubstMap T T]  {s} {σ : Subst T} : +1 ∘ (s :: σ) = σ := by
-        simp [Subst.cons]
-        funext; case _ x =>
-        cases x; all_goals (simp [Subst.compose, Subst.succ])
-
-      @[simp, grind =]
-      theorem rewrite5 [SubstMap T T] {σ : Subst T} : σ.act 0 :: (+1 ∘ σ) = σ := by
-        simp [Subst.cons, Subst.compose]; congr
-        funext; case _ x =>
-        cases x <;> simp
-    end
 
-    @[simp, grind =]
-    theorem apply_I_is_id [RenMap T] [SubstMap S T] [SubstMapId S T] {s : S}
-      : s[+0:T] = s
-    := SubstMapId.apply_id
+universe u1 u2 u3
+variable {S : Type u1} {T : Type u2} {U : Type u3}
 
-    @[simp, grind =]
-    theorem rewrite_lift [RenMap T] [SubstMap T T] [SubstMapStable T] {σ : Subst T}
-      : σ.lift = re 0 :: (σ ∘ +1)
-    := by
-      simp [Subst.cons, Subst.lift, Subst.compose]
-      funext; case _ x =>
-      cases x; simp
-      case _ n =>
-        simp [Subst.succ]
-        generalize tdef : σ.act n = t
-        cases t <;> simp at *
-        case _ y =>
-          rw [apply_stable (σ := +1)]
-          simp [Subst.succ]
-          rw [Ren.to_succ]
+class RenMapId (S : Type u1) (T : Type u2) [RenMap S T] where
+  apply_id {s : S} : s⟨.id T⟩ = s
 
-    @[simp, grind =]
-    theorem rewrite_lift_zero [RenMap S] [RenMapId S] {σ : Subst S}
-      : σ.lift 0 = σ
-    := by
-      simp [Subst.lift]; congr; funext; case _ i =>
-      generalize zdef : σ.act i = z
-      cases z <;> simp [Ren.add]; case _ s =>
-      have lem := RenMapId.apply_id (t := s)
-      simp [Ren.id] at lem; exact lem
-
-    @[grind =]
-    theorem rewrite_lift_succ
-      [RenMap S] [RenMapId S] [RenMapCompose S]
-      {k} {σ : Subst S}
-      : σ.lift (k + 1) = (σ.lift k).lift
-    := by
-      induction k; simp
-      case _ n ih =>
-        replace ih i : (σ.lift (n + 1)).act i = ((σ.lift n).lift 1).act i := by rw [ih]
-        simp [Subst.lift]
-        funext; case _ i =>
-        have lem := ih i
-        cases i <;> simp
-        case _ i =>
-          simp [Subst.lift] at lem
-          split; simp; case _ h1 =>
-          simp at h1
-          have lem2 : n ≤ i := by omega
-          generalize zdef : σ.act (i - (n + 1)) = z
-          cases z <;> simp; omega
-          congr
+class RenMapCompose (S : Type u1) (T : Type u2) [RenMap S T] where
+  apply_compose {s : S} {r1 r2 : Ren T} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩
 
-    @[simp, grind =]
-    theorem rewrite6 [RenMap T] [SubstMap T T] [SubstMapId T T] {σ : Subst T}
-      : σ ∘ +0 = σ
-    := by
-      simp [Subst.compose, Subst.id]; congr
-      funext; case _ x =>
-      generalize zdef : σ.act x = z
-      cases z <;> simp at *; case _ s =>
-      have lem := SubstMapId.apply_id (T := T) (t := s)
-      simp [Subst.id] at lem; exact lem
+@[simp]
+theorem Ren.apply_id [RenMap S T] [RenMapId S T] {s : S} : s⟨id T⟩ = s := RenMapId.apply_id
 
-    @[simp, grind =]
-    theorem apply_compose
-      [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T]
-      {s : S} {σ τ : Subst T}
-      : s[σ:T][τ:_] = s[σ ∘ τ:T]
-    := SubstMapCompose.apply_compose
+@[simp, grind =]
+theorem Ren.apply_compose [RenMap S T] [RenMapCompose S T] {s : S} {r1 r2 : Ren T}
+  : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩
+:= RenMapCompose.apply_compose
 
-    @[simp, grind =]
-    theorem rewrite7
-      [RenMap T] [SubstMap T T] [SubstMapCompose T T]
-      {σ τ μ : Subst T}
-      : (σ ∘ τ) ∘ μ = σ ∘ τ ∘ μ
-    := by
-      simp [Subst.compose]
-      funext; case _ x =>
-      cases σ.act x <;> simp [Subst.compose]
+instance (priority := high) [RenMap T T] [RenMapId T T] : RenMapId (Action T) T where
+  apply_id := by intro s; cases s <;> simp
 
-    @[simp, grind =]
-    theorem hrewrite1
-      [RenMap T] [SubstMap S T] [SubstMapId S T]
-      {σ : Subst S}
-      : σ ◾ (+0@T) = σ
-    := by
-      simp [Subst.hcompose]; congr
-      funext; case _ x =>
-      generalize zdef : σ.act x = z
-      cases z <;> simp
+instance [RenMap S T] [RenMapId S T] : RenMapId (Action S) T where
+  apply_id := by intro s; cases s <;> simp
 
-    @[simp, grind =]
-    theorem hcomp_ren_left
-      [RenMap S] [RenMap T] [SubstMap S T]
-      (r : Ren) (σ : Subst T)
-      : (@Ren.to S r) ◾ σ = r.to
-    := by
-      funext; case _ x =>
-      induction x <;> simp [Subst.hcompose, Ren.to]
+instance (priority := high) [RenMap T T] [RenMapCompose T T] : RenMapCompose (Action T) T where
+  apply_compose := by intro s; cases s <;> simp
 
-    @[simp, grind =]
-    theorem hrewrite2
-      [RenMap S] [RenMap T] [SubstMap S T]
-      {σ : Subst T}
-      : (+0@S) ◾ σ = +0
-    := by
-      apply hcomp_ren_left (S := S) (T := T) Ren.id σ
+instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (Action S) T where
+  apply_compose := by intro s; cases s <;> simp
 
-    @[simp, grind =]
-    theorem hrewrite3
-      [RenMap S] [RenMap T] [SubstMap S T]
-      {σ : Subst T}
-      : (+1@S) ◾ σ = +1
-    := by
-      have lem := hcomp_ren_left (S := S) (T := T) (Ren.add 1) σ
-      simp at lem; exact lem
+class SubstMapId (S : Type u1) (T : Type u2) [SubstMap S T] where
+  apply_id {s : S} : s[.id T] = s
 
-    @[simp, grind =]
-    theorem hrewrite4
-      [RenMap T] [SubstMap S T]
-      {x} {σ : Subst S} {τ : Subst T}
-      : (re x :: σ) ◾ τ = re x :: (σ ◾ τ)
-    := by
-      simp [Subst.hcompose]; congr
-      funext; case _ i =>
-      cases i <;> simp [Subst.cons]
+class SubstMapStable (S : Type u1) (T : Type u2) [RenMap S T] [SubstMap S T] where
+  apply_stable (r : Ren T) (σ : Subst T) : r.to = σ -> rmap (S := S) r = smap σ
 
-    @[grind =]
-    theorem hcomp_dist_ren_left
-      [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
-      (r : Ren) {σ : Subst S} {τ : Subst T}
-      : (r.to ∘ σ) ◾ τ = r.to ∘ σ ◾ τ
-    := by
-      funext; case _ x =>
-      simp [Subst.hcompose, Subst.compose, Ren.to]
+class SubstMapRenComposeLeft (S : Type u1) (T : Type u2) [RenMap S T] [SubstMap S T] where
+  apply_ren_compose_left {s : S} {r : Ren T} {τ : Subst T} : s⟨r⟩[τ] = s[r ∘ τ]
+
+class SubstMapRenComposeRight (T : Type u2) [RenMap T T] [SubstMap T T] where
+  apply_ren_compose_right {t : T} {r : Ren T} {σ : Subst T} : t[σ]⟨r⟩ = t[σ ∘ r]
+
+class SubstMapCompose (S : Type u1) (T : Type u2) [SubstMap S T] [SubstMap T T] where
+  apply_compose {s : S} {σ τ : Subst T} : s[σ][τ] = s[σ ∘ τ]
 
+class SubstMapRenCommute (S : Type u1) (T : Type u2) [RenMap S S] [SubstMap S T] where
+  apply_ren_commute {s : S} (r : Ren S) (τ : Subst T) : s⟨r⟩[τ] = s[τ]⟨r⟩
+
+class SubstMapHetCompose (S : Type u1) (T : Type u2) [SubstMap S S] [SubstMap S T] where
+  apply_hcompose {s : S} {σ : Subst S} {τ : Subst T} : s[σ][τ] = s[τ][σ ◾ τ]
+
+namespace Subst
+  export SubstMapStable (apply_stable)
+  export SubstMapRenComposeLeft (apply_ren_compose_left)
+  export SubstMapRenComposeRight (apply_ren_compose_right)
+  export SubstMapRenCommute (apply_ren_commute)
+end Subst
+
+@[grind <-]
+theorem Ren.lift_eq_from_eq [RenMap T T] {r : Ren T} {σ : Subst T}
+  : r.to = σ -> r.to.lift = σ.lift
+:= by intro h; rw [<-h]
+
+namespace Subst
+  section
     @[simp, grind =]
-    theorem hrewrite5
-      [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T]
-      {σ : Subst S} {τ μ : Subst T}
-      : (σ ◾ τ) ◾ μ = σ ◾ (τ ∘ μ)
-    := by
-      simp [Subst.hcompose]
-      funext; case _ x =>
-      generalize zdef : σ.act x = z
-      cases z <;> simp
-
-    @[grind =]
-    theorem hcomp_distr_ren_right
-      [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
-      [SubstMapStable S] [SubstMapRenCommute S T]
-      (r : Ren) (σ : Subst S) (μ : Subst T)
-      : (σ ∘ r.to) ◾ μ = (σ ◾ μ) ∘ r.to
-    := by
-      simp [Subst.hcompose, Subst.compose, Ren.to]
+    theorem rewrite1 : re 0 :: +1 = id T := by
+      simp [Subst.cons, Subst.id]
       funext; case _ x =>
-      generalize zdef : σ.act x = z
-      cases z <;> simp
-      rw [<-apply_stable r ⟨λ n => re (r.act n)⟩ rfl]
-      rw [SubstMapRenCommute.apply_ren_commute r μ]
-
-    @[grind =]
-    theorem hcomp_distr_ren_right_p1
-      [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
-      [SubstMapStable S] [SubstMapRenCommute S T]
-      (σ : Subst S) (μ : Subst T)
-      : (σ ∘ +1) ◾ μ = (σ ◾ μ) ∘ +1
-    := by
-      have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp
-      rw [lem, hcomp_distr_ren_right]
+      cases x; all_goals simp
+
+    open SubstMap
 
     @[simp, grind =]
-    theorem hrewrite6
-      [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
-      [SubstMapStable S] [SubstMapRenCommute S T]
-      (r : Ren) (σ : Subst S)
-      : (σ ∘ r.to) ◾ (+1@T) = (σ ◾ +1@T) ∘ r.to
-    := by
-      have lem := hcomp_distr_ren_right (T := T) r σ +1
-      simp at lem; exact lem
+    theorem I_lift [RenMap T T] {k} : +0.lift k = id T := by
+      funext; case _ x =>
+      cases x; all_goals (simp [Subst.lift, Subst.id])
+      grind
 
     @[simp, grind =]
-    theorem apply_hcompose
-      [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
-      {s : S} {σ : Subst S} {τ : Subst T}
-      : s[σ][τ:T] = s[τ:T][σ ◾ τ]
-    := by exact SubstMapHetCompose.apply_hcompose
+    theorem rewrite2 [SubstMap T T] {σ : Subst T} : +0 ∘ σ = σ := by
+      funext; case _ x =>
+      unfold Subst.compose; simp [Subst.id]
 
     @[simp, grind =]
-    theorem hrewrite7
-      [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
-      {σ τ : Subst S} (μ : Subst T)
-      : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ
+    theorem rewrite3_replace [SubstMap T T] {σ τ : Subst T} {s : T}
+      : (su s :: σ) ∘ τ = su s[τ] :: (σ ∘ τ)
     := by
-      simp [Subst.hcompose, Subst.compose]
+      simp [Subst.cons, Subst.compose]
       funext; case _ x =>
-      generalize zdef : σ.act x = z
-      cases z <;> simp [Subst.hcompose]
+      cases x; all_goals simp
 
-    theorem hrewrite_lift1
-      [RenMap S] [RenMap T] [SubstMap S T] [SubstMapRenCommute S T]
-      {σ : Subst S} {τ : Subst T}
-      : (σ ◾ τ).lift = σ.lift ◾ τ
+    @[simp, grind =]
+    theorem rewrite3_rename [SubstMap T T] {s} {σ τ : Subst T}
+      : (re s :: σ) ∘ τ = (τ.act s) :: (σ ∘ τ)
     := by
-      simp [Subst.lift]; congr; funext; case _ i =>
-      cases i <;> simp [hcompose]
-      case _ n =>
-        generalize zdef : σ.act n = z
-        cases z <;> simp; case _ t =>
-        rw [SubstMapRenCommute.apply_ren_commute]
+      simp [Subst.cons, Subst.compose]
+      funext; case _ x =>
+      cases x; all_goals simp
 
     @[simp, grind =]
-    theorem hrewrite_lift
-      [RenMap S] [RenMap T] [SubstMap S T] [RenMapId S] [RenMapCompose S] [SubstMapRenCommute S T]
-      {k} {σ : Subst S} {τ : Subst T}
-      : (σ ◾ τ).lift k = σ.lift k ◾ τ
-    := by
-      induction k generalizing σ τ
-      case _ => simp
-      case _ i ih =>
-        rw [rewrite_lift_succ]
-        rw [rewrite_lift_succ]
-        simp; rw [ih, hrewrite_lift1]
-        grind
-  end Subst
+    theorem rewrite4 [SubstMap T T]  {s} {σ : Subst T} : +1 ∘ (s :: σ) = σ := by
+      simp [Subst.cons]
+      funext; case _ x =>
+      cases x; all_goals (simp [Subst.compose, Subst.succ])
 
-  @[grind =]
-  theorem Subst.Compose.lemma1
-    [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S]
-    {k} {τ : Subst S}
-    : (Ren.to (Ren.add 1)) ∘ τ.lift (k + 1) = τ.lift k ∘ (Ren.to (Ren.add 1))
-  := by
-    simp [Subst.compose]
-    funext; case _ x =>
-    cases x
-    all_goals
-      unfold Subst.lift; simp
-      split; simp; split
-    any_goals solve | congr 1
-    all_goals
-      rw [<-apply_stable _ +1 rfl]
-      simp; congr
+    @[simp, grind =]
+    theorem rewrite5 [SubstMap T T] {σ : Subst T} : σ.act 0 :: (+1 ∘ σ) = σ := by
+      simp [Subst.cons, Subst.compose]; congr
+      funext; case _ x =>
+      cases x <;> simp
+  end
 
-  @[grind =]
-  theorem Subst.Compose.lemma1s
-    [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S]
-    {k} {τ : Subst S}
-    : +1 ∘ τ.lift (k + 1) = τ.lift k ∘ +1
-  := by
-    have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp
-    rw [lem]; grind
+  @[simp, grind =]
+  theorem apply_I_is_id [SubstMap S T] [SubstMapId S T] {s : S}
+    : s[id T] = s
+  := SubstMapId.apply_id
 
-  @[grind =]
-  theorem Subst.Compose.lemma2_k1
-    [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S]
-    {σ : Subst S} {r : Ren}
-    : (r ∘ σ).lift = (Ren.to r).lift ∘ σ.lift
+  @[simp, grind =]
+  theorem rewrite_lift [RenMap T T] [SubstMap T T] [SubstMapStable T T] {σ : Subst T}
+    : σ.lift = re 0 :: (σ ∘ +1)
   := by
-    simp [Subst.lift, Subst.compose, Ren.to]
+    simp [Subst.cons, Subst.lift, Subst.compose]
     funext; case _ x =>
-    cases x <;> simp
-
-  @[grind =]
-  theorem Subst.Compose.lemma2
-    [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S]
-    {k} {σ : Subst S} {r : Ren}
-    : (r ∘ σ).lift k = (Ren.to r).lift k ∘ σ.lift k
-  := by
-    induction k generalizing r σ; simp
-    case _ k ih =>
-    rw [Subst.rewrite_lift_succ, ih]
-    rw [<-Ren.to_lift, Subst.Compose.lemma2_k1]
-    rw [Subst.rewrite_lift_succ (σ := r.to)]
-    rw [Subst.rewrite_lift_succ (σ := σ)]
-    grind
+    cases x; simp
+    case _ n =>
+      simp [Subst.succ]
+      generalize tdef : σ.act n = t
+      cases t <;> simp at *
+      case _ y =>
+        rw [apply_stable (σ := +1)]
+        simp [Subst.succ]
+        rw [Ren.to_succ]
 
-  @[grind =]
-  theorem Subst.Compose.lemma2s
-    [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S]
-    {k} {σ : Subst S}
-    : (+1 ∘ σ).lift k = +1.lift k ∘ σ.lift k
-  := by
-    have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp
-    rw [lem]; grind
+  @[simp, grind =]
+  theorem rewrite_lift_zero [RenMap T T] [RenMapId T T] {σ : Subst T}
+    : σ.lift 0 = σ
+  := by simp [Subst.lift]
 
   @[grind =]
-  theorem Subst.Compose.lemma3
-    [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapRenComposeLeft S T]
-    {s : S} {σ : Subst T}
-    : s[+1:T][σ:_] = s[+1 ∘ σ:_]
+  theorem rewrite_lift_succ
+    [RenMap T T] [RenMapId T T] [RenMapCompose T T]
+    {k} {σ : Subst T}
+    : σ.lift (k + 1) = (σ.lift k).lift
   := by
-    have lem : @Subst.succ T = Ren.to (Ren.add 1) := by simp
-    rw [lem, apply_ren_compose_left]
+    induction k; simp
+    case _ n ih =>
+      replace ih i : (σ.lift (n + 1)).act i = ((σ.lift n).lift 1).act i := by rw [ih]
+      simp [Subst.lift]
+      funext; case _ i =>
+      have lem := ih i
+      cases i <;> simp
+      case _ i =>
+        simp [Subst.lift] at lem
+        split; simp; case _ h1 =>
+        simp at h1
+        have lem2 : n ≤ i := by omega
+        generalize zdef : σ.act (i - (n + 1)) = z
+        cases z <;> simp; omega
+        congr
 
-  @[grind =]
-  theorem Subst.Compose.lemma4
-    [RenMap T] [SubstMap T T]
-    {σ τ : Subst T}
-    : +1 ∘ τ ∘ σ = (+1 ∘ τ) ∘ σ
+  @[simp, grind =]
+  theorem rewrite6 [RenMap T T] [SubstMap T T] [SubstMapId T T] {σ : Subst T}
+    : σ ∘ +0 = σ
   := by
+    simp [Subst.compose, Subst.id]; congr
     funext; case _ x =>
-    cases x <;> simp [Subst.compose, Subst.succ]
+    generalize zdef : σ.act x = z
+    cases z <;> simp at *; case _ s =>
+    have lem := SubstMapId.apply_id (T := T) (s := s)
+    simp [Subst.id] at lem; exact lem
 
-  @[grind =]
-  theorem Subst.compose.lemma5
-    [RenMap T] [SubstMap T T] [RenMapCompose T] [SubstMapStable T]
-    {r1 r2 : Ren} {τ : Subst T}
-    : (τ ∘ r2.to) ∘ r1.to = τ ∘ r2.to ∘ r1.to
+  @[simp, grind =]
+  theorem apply_compose [SubstMap S T] [SubstMap T T] [SubstMapCompose S T] {s : S} {σ τ : Subst T}
+    : s[σ][τ] = s[σ ∘ τ]
+  := SubstMapCompose.apply_compose
+
+  @[simp, grind =]
+  theorem rewrite7
+    [SubstMap T T] [SubstMapCompose T T]
+    {σ τ μ : Subst T}
+    : (σ ∘ τ) ∘ μ = σ ∘ τ ∘ μ
   := by
     simp [Subst.compose]
     funext; case _ x =>
-    cases τ.act x <;> simp [*]
-    simp [Ren.to]
-    rw [<-apply_stable r2 ⟨λ n => re (r2.act n)⟩ rfl]
-    rw [<-apply_stable r1 ⟨λ n => re (r1.act n)⟩ rfl]
-    simp
-    rw [apply_stable _ _ rfl]
-    rw [Ren.to_compose]
-    unfold Subst.compose; simp [Ren.to]
+    cases σ.act x <;> simp [Subst.compose]
 
-  @[grind =]
-  theorem Subst.Compose.lemma6_k1
-    [RenMap S] [SubstMap S S] [SubstMapStable S] [SubstMapRenComposeLeft S S]
-    {σ : Subst S} {r : Ren}
-    : (σ ∘ r.to).lift = σ.lift ∘ (Ren.to r).lift
-  := by
-    simp [Subst.lift, Subst.compose]
+  @[simp, grind =]
+  theorem hrewrite1 [SubstMap S T] [SubstMapId S T] {σ : Subst S} : σ ◾ (id T) = σ := by
+    simp [Subst.hcompose]; congr
     funext; case _ x =>
-    cases x <;> simp
-    case _ x =>
-      cases σ.act x <;> simp
-      rw [apply_stable (Ren.add 1) _ rfl]
-      rw [apply_ren_compose_left]
-      rw [apply_ren_compose_left]
-      simp [Ren.to, Subst.compose, Ren.add]
+    generalize zdef : σ.act x = z
+    cases z <;> simp
 
-  @[grind =]
-  theorem Subst.Compose.lemma6
-    [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S]
-    [SubstMapStable S] [SubstMapRenComposeLeft S S]
-    {k} {σ : Subst S} {r : Ren}
-    : (σ ∘ r.to).lift k = σ.lift k ∘ (Ren.to r).lift k
-  := by
-    induction k generalizing r σ; simp
-    case _ k ih =>
-    rw [Subst.rewrite_lift_succ, ih]
-    rw [<-Ren.to_lift, Subst.Compose.lemma6_k1]
-    rw [Subst.rewrite_lift_succ (σ := r.to)]
-    rw [Subst.rewrite_lift_succ (σ := σ)]
-    grind
+  -- @[simp, grind =]
+  -- theorem hcomp_ren_left
+  --   [RenMap S] [RenMap T] [SubstMap S T]
+  --   (r : Ren) (σ : Subst T)
+  --   : (@Ren.to S r) ◾ σ = r.to
+  -- := by
+  --   funext; case _ x =>
+  --   induction x <;> simp [Subst.hcompose, Ren.to]
 
-  @[grind =]
-  theorem Subst.Compose.lemma6s
-    [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S]
-    [SubstMapStable S] [SubstMapRenComposeLeft S S]
-    {k} {σ : Subst S}
-    : (σ ∘ +1).lift k = σ.lift k ∘ +1.lift k
-  := by
-    have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp
-    rw [lem]; grind
+  @[simp, grind =]
+  theorem hrewrite2 [SubstMap S T] {σ : Subst T} : (id S) ◾ σ = +0 := by simp [hcompose, id]
 
-  @[grind =]
-  theorem Subst.Compose.lemma7
-    [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapRenComposeRight S T]
-    {s : S} {τ : Subst T}
-    : s[τ:_][+1:T] = s[τ ∘ +1:_]
+  @[simp, grind =]
+  theorem hrewrite3 [SubstMap S T] {σ : Subst T} : (succ S) ◾ σ = +1 := by simp [hcompose, succ]
+
+  @[simp, grind =]
+  theorem hrewrite4
+    [SubstMap S T]
+    {x} {σ : Subst S} {τ : Subst T}
+    : (re x :: σ) ◾ τ = re x :: (σ ◾ τ)
   := by
-    have lem : @Subst.succ T = Ren.to (Ren.add 1) := by simp
-    rw [lem, apply_ren_compose_right]
+    simp [Subst.hcompose]; congr
+    funext; case _ i =>
+    cases i <;> simp [Subst.cons]
 
   @[grind =]
-  theorem Subst.Compose.lemma8
-    [RenMap T] [SubstMap T T] [SubstMapRenComposeLeft T T]
-    {σ τ : Subst T}
-    : (σ ∘ +1) ∘ τ = σ ∘ +1 ∘ τ
+  theorem hcomp_dist_ren_left
+    [SubstMap S T]
+    (r : Ren S) {σ : Subst S} {τ : Subst T}
+    : (r ∘ σ) ◾ τ = r ∘ σ ◾ τ
   := by
-    simp [Subst.compose]
     funext; case _ x =>
-    cases σ.act x <;> simp at *
-    rw [lemma3]
-    unfold Subst.compose; simp
+    simp [hcompose, compose_ren_left]
 
-  @[grind =]
-  theorem Subst.Compose.lemma9
-    [RenMap T] [SubstMap T T] [SubstMapRenComposeRight T T]
-    {σ τ : Subst T}
-    : ((σ ∘ τ) ∘ +1) = σ ∘ τ ∘ +1
+  @[simp, grind =]
+  theorem hrewrite5
+    [SubstMap S T] [SubstMap T T] [SubstMapCompose S T]
+    {σ : Subst S} {τ μ : Subst T}
+    : (σ ◾ τ) ◾ μ = σ ◾ (τ ∘ μ)
   := by
-    simp [Subst.compose]
+    simp [Subst.hcompose]
     funext; case _ x =>
-    cases σ.act x <;> simp at *
-    rw [lemma7]
-    unfold Subst.compose; simp
+    generalize zdef : σ.act x = z
+    cases z <;> simp
 
   @[grind =]
-  theorem Subst.Compose.lemma10
-    [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
-    [SubstMapStable S] [SubstMapRenCommute S T]
-    {σ : Subst S} {μ : Subst T} {r : Ren}
-    : (σ ∘ r.to) ◾ μ = (σ ◾ μ) ∘ r.to
+  theorem hcomp_distr_ren_right
+    [RenMap S S] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T]
+    (r : Ren S) (σ : Subst S) (μ : Subst T)
+    : (σ ∘ r) ◾ μ = (σ ◾ μ) ∘ r
+  := by
+    simp [hcompose, compose_ren_right]; funext; case _ x =>
+    generalize zdef : σ.act x = z
+    cases z <;> simp
+    rw [apply_ren_commute]
+
+  @[simp, grind =]
+  theorem apply_hcompose
+    [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
+    {s : S} {σ : Subst S} {τ : Subst T}
+    : s[σ][τ] = s[τ][σ ◾ τ]
+  := by exact SubstMapHetCompose.apply_hcompose
+
+  @[simp, grind =]
+  theorem hrewrite7
+    [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
+    {σ τ : Subst S} (μ : Subst T)
+    : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ
   := by
     simp [Subst.hcompose, Subst.compose]
     funext; case _ x =>
     generalize zdef : σ.act x = z
-    cases z <;> simp [Ren.to]
-    rw [<-apply_stable r ⟨λ n => re (r.act n)⟩ rfl]
-    rw [Subst.apply_ren_commute]
+    cases z <;> simp [Subst.hcompose]
 
-  @[grind =]
-  theorem Subst.Compose.lemma10s
-    [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
-    [SubstMapStable S] [SubstMapRenCommute S T]
-    {σ : Subst S} {μ : Subst T}
-    : (σ ∘ +1) ◾ μ = (σ ◾ μ) ∘ +1
+  theorem hrewrite_lift1
+    [RenMap S S] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] [SubstMapRenCommute S T]
+    {σ : Subst S} {τ : Subst T}
+    : (σ ◾ τ).lift = σ.lift ◾ τ
   := by
-    have lem := lemma10 (σ := σ) (μ := μ) (r := (Ren.add 1))
-    simp at lem; exact lem
-
-  theorem Subst.rewrite_lift_compose_k1
-    [RenMap T] [SubstMap T T] [SubstMapStable T]
-    [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T]
-    {σ τ : Subst T}
-    : (σ ∘ τ).lift = σ.lift ∘ τ.lift
-  := by
-    simp [Subst.lift, Subst.compose]
-    funext; case _ x =>
-    cases x <;> simp
-    case _ x =>
-    cases σ.act x <;> simp
-    rw [apply_stable _ (Ren.add 1) rfl]; simp
-    rw [Compose.lemma7, Compose.lemma3]
-    simp [Subst.compose]
+    simp [Subst.lift]; congr; funext; case _ i =>
+    cases i <;> simp
+    case _ n =>
+      generalize zdef : σ.act n = z
+      cases z <;> simp; case _ t =>
+      rw [SubstMapRenCommute.apply_ren_commute]
 
   @[simp, grind =]
-  theorem Subst.rewrite_lift_compose
-    [RenMap T] [SubstMap T T] [RenMapId T] [RenMapCompose T] [SubstMapStable T]
-    [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T]
-    {k} {σ τ : Subst T}
-    : (σ ∘ τ).lift k = σ.lift k ∘ τ.lift k
+  theorem hrewrite_lift
+    [RenMap S S] [SubstMap S S] [SubstMap S T] [RenMapId S S] [RenMapCompose S S]
+    [SubstMapHetCompose S T] [SubstMapRenCommute S T]
+    {k} {σ : Subst S} {τ : Subst T}
+    : (σ ◾ τ).lift k = σ.lift k ◾ τ
   := by
-    induction k generalizing σ τ; simp
-    case _ k ih =>
-      rw [rewrite_lift_succ, ih]
-      rw [rewrite_lift_succ (σ := σ)]
-      rw [rewrite_lift_succ (σ := τ)]
-      rw [rewrite_lift_compose_k1]
-
-  macro "subst_solve_id" : tactic => `(tactic| {
-    intro t; induction t
-    any_goals solve | simp +instances [*]
-    all_goals try simp at *; simp  +instances [*]; grind
-  })
-
-  macro "subst_solve_stable" : tactic => `(tactic| {
-    intro r σ h
-    funext; case _ t =>
-    induction t generalizing r σ
-    all_goals simp [rmap, smap, *] at *; try simp +instances [*]
-    any_goals solve | (rw [<-h]; simp +instances [Ren.to])
-    all_goals try repeat funext; grind
-  })
-
-  macro "subst_solve_compose" : tactic => `(tactic| {
-    intro s σ τ
-    induction s generalizing σ τ
-    any_goals solve | simp +instances [*]
-    try any_goals solve | (
-      try simp [-Subst.rewrite_lift, *]
-      try funext; case _ x =>
-      try rw [<-Ren.to_lift]
-      try simp [-Subst.rewrite_lift, *]
-      try grind)
-  })
+    induction k generalizing σ τ
+    case _ => simp
+    case _ i ih =>
+      rw [rewrite_lift_succ]
+      rw [rewrite_lift_succ]
+      simp; rw [ih, hrewrite_lift1]
+      grind
+end Subst
+
+@[grind =]
+theorem Subst.compose_commute_succ [RenMap T T] {τ : Subst T}
+  : τ ∘ Ren.succ T = Ren.succ T ∘ τ.lift
+:= by congr
+
+@[grind =]
+theorem Ren.compose_commute_succ {r : Ren T} : r ∘ succ T = succ T ∘ r.lift := by simp [compose]
+
+theorem Subst.rewrite_lift_compose_ren_left_k1 [RenMap T T] {r : Ren T} {τ : Subst T}
+  : (r ∘ τ).lift = r.lift ∘ τ.lift
+:= by
+  simp [compose_ren_left, lift, Ren.lift]
+  funext; case _ x =>
+  cases x <;> simp
+
+@[simp, grind =]
+theorem Subst.rewrite_lift_compose_ren_left
+  [RenMap T T] [RenMapId T T] [RenMapCompose T T]
+  {k} {r : Ren T} {τ : Subst T}
+  : (r ∘ τ).lift k = r.lift k ∘ τ.lift k
+:= by
+  induction k generalizing r τ; congr
+  case _ k ih =>
+    rw [rewrite_lift_succ, ih]
+    rw [rewrite_lift_compose_ren_left_k1]
+    rw [<-rewrite_lift_succ]
+    rw [<-Ren.lift_of_succ]
+
+theorem Subst.lift_compose_ren_right_k1
+  [RenMap T T] [RenMapId T T] [RenMapCompose T T]
+  {σ : Subst T} {r : Ren T}
+  : (σ ∘ r).lift = σ.lift ∘ r.lift
+:= by
+  simp [lift]; congr; funext; case _ x =>
+  cases x <;> simp; case _ x =>
+  grind
+
+@[simp, grind =]
+theorem Subst.lift_compose_ren_right
+  [RenMap T T] [RenMapId T T] [RenMapCompose T T]
+  {k} {σ : Subst T} {r : Ren T}
+  : (σ ∘ r).lift k = σ.lift k ∘ r.lift k
+:= by
+  induction k generalizing σ r; simp
+  case _ k ih =>
+    rw [rewrite_lift_succ, ih]
+    rw [lift_compose_ren_right_k1]
+    rw [<-rewrite_lift_succ]
+    rw [<-Ren.lift_of_succ]
+
+theorem Subst.rewrite_lift_compose_k1
+  [RenMap T T] [SubstMap T T] [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T]
+  {σ τ : Subst T}
+  : (σ ∘ τ).lift = σ.lift ∘ τ.lift
+:= by
+  simp [compose, lift]
+  funext; case _ x =>
+  cases x <;> simp
+  case _ x =>
+  cases σ.act x <;> simp; case _ t =>
+  rw [SubstMapRenComposeLeft.apply_ren_compose_left]
+  rw [SubstMapRenComposeRight.apply_ren_compose_right]
+  have lem := Subst.compose_commute_succ (τ := τ)
+  simp [lift] at lem
+  rw [lem]
+
+@[simp, grind =]
+theorem Subst.rewrite_lift_compose
+  [RenMap T T] [RenMapId T T] [RenMapCompose T T] [SubstMap T T]
+  [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T]
+  {k} {σ τ : Subst T}
+  : (σ ∘ τ).lift k = σ.lift k ∘ τ.lift k
+:= by
+  induction k generalizing σ τ; simp
+  case _ k ih =>
+    rw [rewrite_lift_succ, ih]
+    rw [rewrite_lift_succ (σ := σ)]
+    rw [rewrite_lift_succ (σ := τ)]
+    rw [rewrite_lift_compose_k1]
+
+macro "subst_solve_id" : tactic => `(tactic| {
+  intro t; induction t
+  any_goals solve | simp +instances [*]
+  all_goals try simp at *; simp  +instances [*]; grind
+})
+
+macro "subst_solve_stable" : tactic => `(tactic| {
+  intro r σ h
+  funext; case _ t =>
+  induction t generalizing r σ
+  all_goals simp [rmap, smap, *] at *; try simp +instances [*]
+  any_goals solve | (rw [<-h]; simp +instances [Ren.to])
+  all_goals try repeat funext; grind
+})
+
+macro "subst_solve_compose" : tactic => `(tactic| {
+  intro s σ τ
+  induction s generalizing σ τ
+  any_goals solve | simp +instances [*]
+  try any_goals solve | (
+    try simp [-Subst.rewrite_lift, *]
+    try funext; case _ x =>
+    try rw [<-Ren.to_lift]
+    try simp [-Subst.rewrite_lift, *]
+    try grind)
+})
 
 end LeanSubst
diff --git a/LeanSubst/Ops.lean b/LeanSubst/Ops.lean
new file mode 100644
index 0000000..7f0136b
--- /dev/null
+++ b/LeanSubst/Ops.lean
@@ -0,0 +1,443 @@
+
+import LeanSubst.Basic
+
+namespace LeanSubst
+
+universe u1 u2 u3
+variable {S : Type u1} {T : Type u2} {U : Type u3}
+
+----------------------------------------------------------------------------------------------------
+---- Action
+----------------------------------------------------------------------------------------------------
+@[simp]
+def Action.rmap [RenMap S T] (r : Ren T) : Action S -> Action S
+| re x => re $ r.act x
+| su t => su t⟨r⟩
+
+instance (priority := high) [RenMap T T] : RenMap (Action T) T where
+  rmap := Action.rmap
+
+@[simp]
+theorem Action.rmap_re [RenMap T T] {r : Ren T} {x : Nat} : (@re T x)⟨r⟩ = re (r.act x) := by
+  simp [RenMap.rmap]
+
+@[simp]
+theorem Action.rmap_su [RenMap T T] {r : Ren T} {t : T} : (su t)⟨r⟩ = su t⟨r⟩ := by
+  simp [RenMap.rmap]
+
+@[simp]
+def Action.hrmap [RenMap S T] (r : Ren T) : Action S -> Action S
+| re x => re x
+| su t => su t⟨r⟩
+
+instance [RenMap S T] : RenMap (Action S) T where
+  rmap := Action.hrmap
+
+@[simp]
+theorem Action.hrmap_re [RenMap S T] {r : Ren T} {x : Nat} : (@re S x)⟨r⟩ = re x := by
+  simp [RenMap.rmap]
+
+@[simp]
+theorem Actionh.rmap_su [RenMap S T] {r : Ren T} {t : S} : (su t)⟨r⟩ = su t⟨r⟩ := by
+  simp [RenMap.rmap]
+
+@[simp]
+def Action.smap [SubstMap T T] (σ : Subst T) : Action T -> Action T
+| re x => σ.act x
+| su t => su t[σ]
+
+instance (priority := high) [SubstMap T T] : SubstMap (Action T) T where
+  smap := Action.smap
+
+@[simp]
+theorem Action.smap_re [SubstMap T T] {σ : Subst T} {x : Nat} : (@re T x)[σ] = σ.act x := by
+  simp [SubstMap.smap]
+
+@[simp]
+theorem Action.smap_su [SubstMap T T] {σ : Subst T} {t : T} : (su t)[σ] = su t[σ] := by
+  simp [SubstMap.smap]
+
+@[simp]
+def Action.hsmap [SubstMap S T] (σ : Subst T) : Action S -> Action S
+| re x => re x
+| su t => su t[σ]
+
+instance [SubstMap S T] : SubstMap (Action S) T where
+  smap := Action.hsmap
+
+@[simp]
+theorem Action.hsmap_re [SubstMap S T] {σ : Subst T} {x : Nat} : (@re S x)[σ] = re x := by
+  simp [SubstMap.smap]
+
+@[simp]
+theorem Actionh.smap_su [SubstMap S T] {σ : Subst T} {t : S} : (su t)[σ] = su t[σ] := by
+  simp [SubstMap.smap]
+----------------------------------------------------------------------------------------------------
+---- Identity
+----------------------------------------------------------------------------------------------------
+def Ren.id T : Ren T := ⟨λ x => x⟩
+
+@[simp]
+theorem Ren.id_action {x} : (id T).act x = x := by simp [Ren.id]
+
+def Subst.id T : Subst T := ⟨λ x => re x⟩
+notation "+0" => Subst.id _
+
+@[simp]
+theorem Subst.id_action {x} : (id T).act x = re x := by simp [Subst.id]
+----------------------------------------------------------------------------------------------------
+---- Successor
+----------------------------------------------------------------------------------------------------
+def Ren.succ T : Ren T := ⟨(· + 1)⟩
+
+@[simp]
+theorem Ren.succ_action {x} : (succ T).act x = x + 1 := by simp [Ren.succ]
+
+def Subst.succ T : Subst T := ⟨λ x => re $ x + 1⟩
+notation "+1" => Subst.succ _
+
+@[simp]
+theorem Subst.succ_action {x} : (succ T).act x = re (x + 1) := by simp [Subst.succ]
+----------------------------------------------------------------------------------------------------
+---- Predecessor
+----------------------------------------------------------------------------------------------------
+def Ren.pred T : Ren T := ⟨(· - 1)⟩
+
+@[simp]
+theorem Ren.pred_action {x} : (pred T).act x = x - 1 := by simp [Ren.pred]
+
+def Subst.pred T : Subst T := ⟨λ x => re $ x - 1⟩
+notation "-1" => Subst.pred _
+
+@[simp]
+theorem Subst.pred_action {x} : (pred T).act x = re (x - 1) := by simp [Subst.pred]
+----------------------------------------------------------------------------------------------------
+---- Addition
+----------------------------------------------------------------------------------------------------
+def Ren.add T (k : Nat) : Ren T := ⟨(· + k)⟩
+
+@[simp]
+theorem Ren.add_action {k x} : (add T k).act x = x + k := by simp [Ren.add]
+
+@[simp]
+theorem Ren.add_zero : add T 0 = id T := by simp [Ren.add, Ren.id]
+
+@[simp]
+theorem Ren.add_one : add T 1 = succ T := by simp [Ren.add, Ren.succ]
+
+def Subst.add T (k : Nat) : Subst T := ⟨λ x => re $ x + k⟩
+
+@[simp]
+theorem Subst.add_action {k x} : (add T k).act x = re (x + k) := by simp [Subst.add]
+
+@[simp]
+theorem Subst.add_zero : add T 0 = +0 := by simp [Subst.add, Subst.id]
+
+@[simp]
+theorem Subst.add_one : add T 1 = +1 := by simp [Subst.add, Subst.succ]
+----------------------------------------------------------------------------------------------------
+---- Subtraction
+----------------------------------------------------------------------------------------------------
+def Ren.sub T (k : Nat) : Ren T := ⟨(· - k)⟩
+
+@[simp]
+theorem Ren.sub_action {k x} : (sub T k).act x = x - k := by simp [Ren.sub]
+
+@[simp]
+theorem Ren.sub_zero : sub T 0 = id T := by simp [Ren.sub, Ren.id]
+
+@[simp]
+theorem Ren.sub_one : sub T 1 = pred T := by simp [Ren.sub, Ren.pred]
+
+def Subst.sub T (k : Nat) : Subst T := ⟨λ x => re $ x - k⟩
+
+@[simp]
+theorem Subst.sub_action {k x} : (@sub T k).act x = re (x - k) := by simp [Subst.sub]
+
+@[simp]
+theorem Subst.sub_zero : sub T 0 = +0 := by simp [Subst.sub, Subst.id]
+
+@[simp]
+theorem Subst.sub_one : sub T 1 = -1 := by simp [Subst.sub, Subst.pred]
+
+----------------------------------------------------------------------------------------------------
+---- Cons
+----------------------------------------------------------------------------------------------------
+def Ren.cons (a : Nat) (r : Ren T) : Ren T := .mk λ n =>
+  match n with
+  | 0 => a
+  | n + 1 => r.act n
+infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons
+
+@[simp]
+theorem Ren.cons_action0 {a} {r : Ren T} : (a::r).act 0 = a := by simp [Ren.cons]
+
+@[simp]
+theorem Ren.cons_action {a i} {r : Ren T} : (a::r).act (i + 1) = r.act i := by simp [Ren.cons]
+
+def Subst.cons (a : Action T) (σ : Subst T) : Subst T := .mk λ n =>
+  match n with
+  | 0 => a
+  | n + 1 => σ.act n
+infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons
+
+@[simp]
+theorem Subst.cons_action0 {a} {σ : Subst T} : (a::σ).act 0 = a := by simp [Subst.cons]
+
+@[simp]
+theorem Subst.cons_action {a i} {σ : Subst T} : (a::σ).act (i + 1) = σ.act i := by simp [Subst.cons]
+----------------------------------------------------------------------------------------------------
+---- Append
+----------------------------------------------------------------------------------------------------
+def Ren.append : List Nat -> Ren T -> Ren T
+| .nil, r => r
+| .cons hd tl, r => hd::append tl r
+
+instance : HAppend (List Nat) (Ren T) (Ren T) where
+  hAppend := Ren.append
+
+@[simp]
+theorem Ren.append_nil {r : Ren T} : ([] : List Nat) ++ r = r := by
+  simp [HAppend.hAppend, Ren.append]
+
+@[simp]
+theorem Ren.append_cons {a} {ℓ : List Nat} {r : Ren T} : (a::ℓ) ++ r = a::(ℓ ++ r) := by
+  simp [HAppend.hAppend, Ren.append]
+
+@[simp, grind <-]
+theorem Ren.append_action_lt {r : Ren T} {i}
+  : {ℓ : List Nat} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i]
+| .cons hd tl, h =>
+  match i with
+  | 0 => rfl
+  | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind)
+
+@[simp, grind <-]
+theorem Ren.append_action_ge {r : Ren T} {i}
+  : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length)
+| .nil, h => by simp
+| .cons hd tl, h =>
+  match i with
+  | 0 => by simp at h
+  | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp)
+
+def Subst.append : List (Action T) -> Subst T -> Subst T
+| .nil, r => r
+| .cons hd tl, r => hd::append tl r
+
+instance : HAppend (List $ Action T) (Subst T) (Subst T) where
+  hAppend := Subst.append
+
+@[simp]
+theorem Subst.append_nil {σ : Subst T} : ([] : List $ Action T) ++ σ = σ := by
+  simp [HAppend.hAppend, Subst.append]
+
+@[simp]
+theorem Subst.append_cons {a} {ℓ : List $ Action T} {σ : Subst T} : (a::ℓ) ++ σ = a::(ℓ ++ σ) := by
+  simp [HAppend.hAppend, Subst.append]
+
+@[simp, grind <-]
+theorem Subst.append_action_lt {σ : Subst T} {i}
+  : {ℓ : List $ Action T} -> (h : i < ℓ.length) -> (ℓ ++ σ).act i = ℓ[i]
+| .cons hd tl, h =>
+  match i with
+  | 0 => rfl
+  | i + 1 => append_action_lt (σ := σ) (ℓ := tl) (by grind)
+
+@[simp, grind <-]
+theorem Subst.append_action_ge {σ : Subst T} {i}
+  : {ℓ : List $ Action T} -> (h : i ≥ ℓ.length) -> (ℓ ++ σ).act i = σ.act (i - ℓ.length)
+| .nil, h => by simp
+| .cons hd tl, h =>
+  match i with
+  | 0 => by simp at h
+  | i + 1 => @append_action_ge σ i tl (by grind) |> cast (by simp)
+----------------------------------------------------------------------------------------------------
+---- Composition
+----------------------------------------------------------------------------------------------------
+def Ren.compose : Ren T -> Ren T -> Ren T
+| r1, r2 => .mk λ n => r2.act (r1.act n)
+infixr:85 " ∘ " => Ren.compose
+
+@[simp]
+theorem Ren.compose_action {r1 r2 : Ren T} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) :=
+  by simp [Ren.compose]
+
+@[simp]
+theorem Ren.compose_id_left {r : Ren T} : id T ∘ r = r := by
+  simp [Ren.compose, Ren.id]
+
+@[simp]
+theorem Ren.compose_id_right {r : Ren T} : r ∘ id T = r := by
+  simp [Ren.compose, Ren.id]
+
+@[simp]
+theorem Ren.compose_assoc {r1 r2 r3 : Ren T} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by
+  simp [Ren.compose]
+
+@[simp]
+theorem Ren.compose_pred_succ : succ T ∘ pred T = id T := by simp [succ, pred, id, compose]
+
+@[simp]
+theorem Ren.compose_sub_add {k} : add T k ∘ sub T k = id T := by simp [sub, add, id, compose]
+
+-- -- r1 contains only S-vars, hence a renaming of T-vars is a no-op
+-- def Ren.hcompose : Ren S -> Ren T -> Ren S
+-- | r, _ => .mk λ n => r.act n
+-- infixr:85 " ◾ " => Ren.hcompose
+
+-- @[simp]
+-- theorem Ren.hcompose_ext {r1 : Ren S} {r2 : Ren T} : r1 ◾ r2 = r1 := sorry
+
+-- -- same deal as `Ren.hcompose`
+-- def Ren.hcompose_subst : Ren S -> Subst T -> Ren S
+-- | r, _ => .mk λ n => r.act n
+-- infixr:85 " ◾ " => Ren.hcompose
+
+def Subst.compose [SubstMap T T] : Subst T -> Subst T -> Subst T
+| σ, τ => .mk λ n => (σ.act n)[τ]
+infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose
+
+@[simp]
+theorem Subst.compose_action [SubstMap T T] {σ τ : Subst T} {x} : (σ ∘ τ).act x = (σ.act x)[τ] := by
+  simp [Subst.compose]
+
+@[simp]
+theorem Subst.compose_pred_succ [SubstMap T T] : succ T ∘ pred T = id T := by
+  simp [succ, pred, id, compose]
+
+@[simp]
+theorem Subst.compose_sub_add [SubstMap T T] {k} : add T k ∘ sub T k = id T := by
+  simp [sub, add, id, compose]
+
+def Subst.compose_ren_left : Ren T -> Subst T -> Subst T
+| r, τ => .mk λ n => τ.act (r.act n)
+infixr:85 (name := Subst.compose_ren_left_notation) " ∘ " => Subst.compose_ren_left
+
+@[simp]
+theorem Subst.compose_ren_left_action {r : Ren T} {τ : Subst T} {x}
+  : (r ∘ τ).act x = τ.act (r.act x)
+:= by simp [Subst.compose_ren_left]
+
+def Subst.compose_ren_right [RenMap T T] : Subst T -> Ren T -> Subst T
+| σ, r => .mk λ n => (σ.act n)⟨r⟩
+infixr:85 (name := Subst.compose_ren_right_notation) " ∘ " => Subst.compose_ren_right
+
+@[simp]
+theorem Subst.compose_ren_right_action [RenMap T T] {σ : Subst T} {r : Ren T} {x}
+  : (σ ∘ r).act x = (σ.act x)⟨r⟩
+:= by simp [Subst.compose_ren_right]
+
+def Subst.hcompose [SubstMap S T] : Subst S -> Subst T -> Subst S
+| σ, τ => .mk λ n => (σ.act n)[τ]
+infixr:85 " ◾ " => Subst.hcompose
+
+@[simp]
+theorem Subst.hcompose_action [SubstMap S T] {σ : Subst S} {τ : Subst T} {x}
+  : (σ ◾ τ).act x = (σ.act x)[τ]
+:= by simp [Subst.hcompose]
+
+def Subst.hcompose_ren [RenMap S T] : Subst S -> Ren T -> Subst S
+| σ, r => .mk λ n => (σ.act n)⟨r⟩
+infixr:85 " ◾ " => Subst.hcompose_ren
+
+@[simp]
+theorem Subst.hcompose_ren_action [RenMap S T] {σ : Subst S} {r : Ren T} {x}
+  : (σ ◾ r).act x = (σ.act x)⟨r⟩
+:= by simp [Subst.hcompose_ren]
+
+----------------------------------------------------------------------------------------------------
+---- Lift
+----------------------------------------------------------------------------------------------------
+def Ren.lift (r : Ren T) (k : Nat := 1) : Ren T := .mk λ n =>
+  if n < k then n else r.act (n - k) + k
+
+@[simp, grind <-]
+theorem Ren.lift_action_lt {r : Ren T} {k i} (h : i < k) : (lift r k).act i = i := by
+  simp [Ren.lift]; grind
+
+@[simp, grind <-]
+theorem Ren.lift_action_ge {r : Ren T} {k i} (h : i ≥ k) : (lift r k).act i = r.act (i - k) + k :=
+  by simp [Ren.lift]; grind
+
+@[simp]
+theorem Ren.lift_of_zero {r : Ren T} : r.lift 0 = r := by
+  unfold Ren.lift; congr
+
+@[grind =]
+theorem Ren.lift_of_succ {r : Ren T} {k} : r.lift (k + 1) = (r.lift k).lift := by
+  induction k; simp
+  case _ n ih =>
+    unfold Ren.lift; congr; funext; case _ i =>
+    simp; unfold Ren.lift at ih; simp at ih
+    grind
+
+@[simp]
+theorem Ren.lift_id {k} : lift (id T) k = id T := by
+  simp [Ren.id, Ren.lift]; congr; funext; case _ x =>
+  cases x <;> simp; omega
+
+theorem Ren.lift_compose1 {r1 r2 : Ren T} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by
+  simp [Ren.compose, Ren.lift]
+  funext; case _ x =>
+  cases x <;> simp
+
+@[simp]
+theorem Ren.lift_compose {k} {r1 r2 : Ren T} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by
+  induction k generalizing r1 r2; simp
+  case _ k ih =>
+    rw [lift_of_succ, ih]
+    rw [lift_of_succ (r := r1)]
+    rw [lift_of_succ (r := r2)]
+    rw [lift_compose1]
+
+def Subst.lift [RenMap T T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n =>
+  if n < k then re n else (σ.act (n - k))⟨.add T k⟩
+
+@[simp, grind <-]
+theorem Subst.lift_action_lt [RenMap T T] {σ : Subst T} {k i} (h : i < k)
+  : (lift σ k).act i = re i
+:= by simp [Subst.lift]; grind
+
+@[simp, grind <-]
+theorem Subst.lift_action_ge [RenMap T T] {σ : Subst T} {k i} (h : i ≥ k)
+  : (lift σ k).act i = (σ.act (i - k))⟨.add T k⟩
+:= by simp [Subst.lift]; grind
+----------------------------------------------------------------------------------------------------
+---- Promotion
+----------------------------------------------------------------------------------------------------
+def Ren.to (r : Ren T) : Subst T := ⟨λ x => re (r.act x)⟩
+
+@[simp]
+theorem Ren.to_act {r : Ren T} {x} : (@to T r).act x = re (r.act x) := by simp [Ren.to]
+
+@[simp]
+theorem Ren.to_id : (id T).to = .id T := by simp [to, id, Subst.id]
+
+@[simp]
+theorem Ren.to_succ : (succ T).to = .succ T := by simp [to, succ, Subst.succ]
+
+@[simp]
+theorem Ren.to_pred : (pred T).to = .pred T := by simp [to, pred, Subst.pred]
+
+@[simp]
+theorem Ren.to_add {k} : (add T k).to = .add T k := by simp [to, add, Subst.add]
+
+@[simp]
+theorem Ren.to_sub {k} : (sub T k).to = .sub T k := by simp [to, sub, Subst.sub]
+
+@[simp]
+theorem Ren.to_lift [RenMap T T] {r : Ren T} {k} : (r.lift k).to = (@to T r).lift k := by
+  cases r; simp [to, lift, Subst.lift]; case _ act =>
+  funext; case _ x =>
+  cases x; grind
+  case _ n => cases Nat.decLt (n + 1) k <;> simp [ite]
+
+@[simp]
+theorem Ren.to_compose [RenMap T T] [SubstMap T T] {r1 r2 : Ren T}
+  : @to T (r1 ∘ r2) = r1.to ∘ r2.to
+:= by
+  funext; case _ x =>
+  cases x <;> simp [to, compose, Subst.compose]
+
+end LeanSubst
diff --git a/LeanSubst/Option.lean b/LeanSubst/Option.lean
deleted file mode 100644
index bf19a5e..0000000
--- a/LeanSubst/Option.lean
+++ /dev/null
@@ -1,45 +0,0 @@
-import LeanSubst.Ren
-import LeanSubst.Subst
-import LeanSubst.Laws
-
-namespace LeanSubst
-
-variable {S T : Type}
-
-def Option.rmap [i : RenMap S] (r : Ren) : Option S -> Option S
-| none => none
-| some t => some (i.rmap r t)
-
-instance [RenMap S] : RenMap (Option S) where
-  rmap := Option.rmap
-
-def Option.smap [SubstMap S T] (σ : Subst T) : Option S -> Option S
-| none => none
-| some t => some t[σ:_]
-
-instance [SubstMap S T] : SubstMap (Option S) T where
-  smap := Option.smap
-
-@[simp, grind =]
-theorem Option.smap_none [SubstMap S T] {σ : Subst T}
-  : (@Option.none S)[σ:_] = none
-:= by
-  simp [SubstMap.smap, Option.smap]
-
-@[simp, grind =]
-theorem Option.smap_some [SubstMap S T] {x : S} {σ : Subst T}
-  : (some x)[σ:_] = some x[σ:_]
-:= by
-  simp [SubstMap.smap, Option.smap]
-
-instance [RenMap T] [SubstMap S T] [SubstMapId S T]
-  : SubstMapId (Option S) T
-where
-  apply_id := by intro t; cases t <;> simp
-
-instance [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T]
-  : SubstMapCompose (Option S) T
-where
-  apply_compose := by intro s σ τ; cases s <;> simp
-
-end LeanSubst
diff --git a/LeanSubst/Ren.lean b/LeanSubst/Ren.lean
deleted file mode 100644
index 2dd13b0..0000000
--- a/LeanSubst/Ren.lean
+++ /dev/null
@@ -1,117 +0,0 @@
-
-namespace LeanSubst
-  universe u
-  variable {S T : Type}
-
-  structure Ren where
-    act : Nat -> Nat
-
-  def Ren.id : Ren := ⟨λ x => x⟩
-
-  def Ren.add (k : Nat) : Ren := ⟨(· + k)⟩
-
-  def Ren.sub (k : Nat) : Ren := ⟨(· - k)⟩
-
-  def Ren.lift (r : Ren) (k : Nat := 1) : Ren := .mk λ n =>
-    if n < k then n else r.act (n - k) + k
-
-  def Ren.cons (a : Nat) (r : Ren) : Ren := .mk λ n =>
-    match n with
-    | 0 => a
-    | n + 1 => r.act n
-
-  def Ren.append : List Nat -> Ren -> Ren
-  | .nil, r => r
-  | .cons hd tl, r => append tl (r.cons hd)
-
-  instance : HAppend (List Nat) Ren Ren where
-    hAppend := Ren.append
-
-  def Ren.compose : Ren -> Ren -> Ren
-  | r1, r2 => .mk λ n => r2.act (r1.act n)
-
-  class RenMap (T : Type) where
-    rmap : Ren -> T -> T
-
-  export RenMap (rmap)
-
-  macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t)
-  infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons
-  infixr:85 (name := Ren.compose_notation) " ∘ " => Ren.compose
-
-  @[app_unexpander rmap]
-  def unexpandRenApply : Lean.PrettyPrinter.Unexpander
-  | `($_ $r $t) => `($t⟨$r⟩)
-  | _ => throw ()
-
-  @[simp, grind =]
-  theorem Ren.lift_zero {r : Ren} : r.lift 0 = r := by
-    unfold Ren.lift; congr
-
-  @[grind =]
-  theorem Ren.lift_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by
-    induction k; simp
-    case _ n ih =>
-      unfold Ren.lift; congr; funext; case _ i =>
-      simp; unfold Ren.lift at ih; simp at ih
-      grind
-
-  @[simp]
-  theorem Ren.id_action {x} : Ren.id.act x = x := by simp [Ren.id]
-
-  @[simp]
-  theorem Ren.lift_id {k} : Ren.lift Ren.id k = Ren.id := by
-    simp [Ren.id, Ren.lift]; congr; funext; case _ x =>
-    cases x <;> simp; omega
-
-  @[simp]
-  theorem Ren.cons_head_action {n} {r : Ren} : (n::r).act 0 = n := by simp [Ren.cons]
-
-  @[simp]
-  theorem Ren.cons_tail_action {n i} {r : Ren} : (n::r).act (i + 1) = r.act i := by simp [Ren.cons]
-
-  @[simp]
-  theorem Ren.compose_id_left {r : Ren} : id ∘ r = r := by
-    simp [Ren.compose, Ren.id]
-
-  @[simp]
-  theorem Ren.compose_id_right {r : Ren} : r ∘ id = r := by
-    simp [Ren.compose, Ren.id]
-
-  @[simp]
-  theorem Ren.compose_assoc {r1 r2 r3 : Ren} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by
-    simp [Ren.compose]
-
-  @[simp]
-  theorem Ren.compose_action {r1 r2 : Ren} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by
-    simp [Ren.compose]
-
-  theorem Ren.compose_lift_k1 {r1 r2 : Ren} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by
-    simp [Ren.compose, Ren.lift]
-    funext; case _ x =>
-    cases x <;> simp
-
-  @[simp]
-  theorem Ren.compose_lift {k} {r1 r2 : Ren} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by
-    induction k generalizing r1 r2; simp
-    case _ k ih =>
-      rw [lift_succ, ih]
-      rw [lift_succ (r := r1)]
-      rw [lift_succ (r := r2)]
-      rw [compose_lift_k1]
-
-  class RenMapId (S : Type) [RenMap S] where
-    apply_id {t : S} : t⟨Ren.id⟩ = t
-
-  class RenMapCompose (S : Type) [RenMap S] where
-    apply_compose {s : S} {r1 r2 : Ren} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩
-
-  @[simp, grind =]
-  theorem Ren.apply_id [RenMap T] [RenMapId T] {t : T} : t⟨id⟩ = t := RenMapId.apply_id
-
-  @[simp, grind =]
-  theorem Ren.apply_compose [RenMap T] [RenMapCompose T] {t : T} {r1 r2 : Ren}
-    : t⟨r1⟩⟨r2⟩ = t⟨r1 ∘ r2⟩
-  := RenMapCompose.apply_compose
-
-end LeanSubst
diff --git a/LeanSubst/Normal.lean b/LeanSubst/Rewriting/Normal.lean
similarity index 96%
rename from LeanSubst/Normal.lean
rename to LeanSubst/Rewriting/Normal.lean
index cb7c8a9..596a13b 100644
--- a/LeanSubst/Normal.lean
+++ b/LeanSubst/Rewriting/Normal.lean
@@ -1,8 +1,7 @@
 
 import Init.WF
-import LeanSubst.Ren
-import LeanSubst.Subst
-import LeanSubst.Reduction
+import LeanSubst.Laws
+import LeanSubst.Rewriting.Reduction
 
 namespace LeanSubst
   universe u
@@ -113,7 +112,7 @@ namespace LeanSubst
         intro a; replace h := h a
         apply equiv_acc.1 h
 
-      variable [RenMap T] [SubstMap T T] [Substitutive R]
+      variable [RenMap T T] [SubstMap T T] [Substitutive R]
 
       theorem subst_preimage {σ : Subst T} {t} : SN R t[σ] -> SN R t := by
         intro r; apply preimage (smap σ) t _ r
diff --git a/LeanSubst/Reduction.lean b/LeanSubst/Rewriting/Reduction.lean
similarity index 97%
rename from LeanSubst/Reduction.lean
rename to LeanSubst/Rewriting/Reduction.lean
index db77ef0..927c24a 100644
--- a/LeanSubst/Reduction.lean
+++ b/LeanSubst/Rewriting/Reduction.lean
@@ -1,11 +1,10 @@
 
-import LeanSubst.Ren
-import LeanSubst.Subst
+import LeanSubst.Laws
 
 namespace LeanSubst
   universe u
 
-  class Substitutive {T : Type} [RenMap T] [SubstMap T T] (R : T -> T -> Prop) where
+  class Substitutive {T : Type} [RenMap T T] [SubstMap T T] (R : T -> T -> Prop) where
     subst {t s} (σ : Subst T) : R t s -> R (t[σ]) (s[σ])
 
   class HasTriangle {T : Type u} (R : T -> T -> Prop) where
@@ -15,7 +14,7 @@ namespace LeanSubst
   section
     variable {T : Type}
 
-    inductive ActionRed (R : T -> T -> Prop) : Subst.Action T -> Subst.Action T -> Prop where
+    inductive ActionRed (R : T -> T -> Prop) : Action T -> Action T -> Prop where
     | su {x y} : R x y -> ActionRed R (.su x) (.su y)
     | re {x} : ActionRed R (.re x) (.re x)
 
@@ -190,7 +189,7 @@ namespace LeanSubst
               exists q; apply And.intro
               apply lem.1; apply Star.step ih.2 lem.2
 
-      variable [RenMap T] [SubstMap T T] [Substitutive R]
+      variable [RenMap T T] [SubstMap T T] [Substitutive R]
 
       omit [HasTriangle R] in
       theorem subst {x y} (σ : Subst T) : Star R x y -> Star R x[σ] y[σ] := by
diff --git a/LeanSubst/Subst.lean b/LeanSubst/Subst.lean
deleted file mode 100644
index a17602e..0000000
--- a/LeanSubst/Subst.lean
+++ /dev/null
@@ -1,137 +0,0 @@
-import LeanSubst.Ren
-
-namespace LeanSubst
-  universe u
-  variable {S T : Type}
-
-  inductive Subst.Action (T : Type) where
-  | re : Nat -> Subst.Action T
-  | su : T -> Subst.Action T
-  deriving Repr
-
-  export Subst.Action (re su)
-
-  structure Subst (T : Type) where
-    act : Nat -> Subst.Action T
-
-  @[coe]
-  def Ren.to : Ren -> Subst T
-  | r  => .mk λ n => re (r.act n)
-
-  instance : Coe Ren (Subst T) where
-    coe := Ren.to
-
-  class SubstMap (S T : Type) where
-    smap : Subst T -> S -> S
-
-  export SubstMap (smap)
-
-  def Subst.lift [RenMap T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n =>
-    if n < k then re n else
-      match σ.act (n - k) with
-      | su t => su (rmap (Ren.add k) t)
-      | re i => re (i + k)
-
-  def Subst.cons (a : Subst.Action T) (σ : Subst T) : Subst T := .mk λ n =>
-    match n with
-    | 0 => a
-    | n + 1 => σ.act n
-
-  def Subst.append : List (Subst.Action T) -> Subst T -> Subst T
-  | .nil, σ => σ
-  | .cons hd tl, σ => append tl (σ.cons hd)
-
-  instance : HAppend (List $ Subst.Action T) (Subst T) (Subst T) where
-    hAppend := Subst.append
-
-  @[simp]
-  abbrev smap1 [SubstMap S S] := smap (S := S) (T := S)
-
-  def Subst.compose [RenMap T] [SubstMap T T] : Subst T -> Subst T -> Subst T
-  | σ, τ => .mk λ n =>
-    match σ.act n with
-    | su t => su (smap τ t)
-    | re k => τ.act k
-
-  def Subst.hcompose [RenMap T] [SubstMap S T] : Subst S -> Subst T -> Subst S
-  | σ, τ => .mk λ n =>
-    match σ.act n with
-    | su t => su (smap τ t)
-    | re k => re k
-
-  def Subst.id : Subst T := ⟨λ n => re n⟩
-  def Subst.succ : Subst T := ⟨λ n => re (n + 1)⟩
-  def Subst.pred : Subst T := ⟨λ n => re (n - 1)⟩
-
-  notation "+0" => Subst.id
-  macro "+0@" noWs T:term : term =>`(@Subst.id $T)
-  notation "+1" => Subst.succ
-  macro "+1@" noWs T:term : term =>`(@Subst.succ $T)
-  notation "-1" => Subst.pred
-  macro "-1@" noWs T:term : term =>`(@Subst.pred $T)
-
-  @[simp, grind =]
-  theorem Subst.id_action {n} : (+0@T).act n = re n := by simp [Subst.id]
-
-  @[simp, grind =]
-  theorem Subst.succ_action {n} : (+1@T).act n = re (n + 1) := by simp [Subst.succ]
-
-  @[simp, grind =]
-  theorem Subst.pred_action {n} : (-1@T).act n = re (n - 1) := by simp [Subst.pred]
-
-  @[simp, grind =]
-  theorem Ren.to_id : Ren.to (T := T) id = +0 := by
-    unfold Ren.to; unfold Subst.id; simp [id]
-
-  @[simp, grind =]
-  theorem Ren.to_succ : Ren.to (T := T) (Ren.add 1) = +1 := by
-    unfold Ren.to; simp; unfold Subst.succ; simp [Ren.add]
-
-  @[simp, grind =]
-  theorem Ren.to_pred : Ren.to (T := T) (Ren.sub 1) = -1 := by
-    unfold Ren.to; simp; unfold Subst.pred; simp [Ren.sub]
-
-  @[simp, grind =]
-  theorem Ren.pred_succ [RenMap T] [SubstMap T T] : Subst.compose (T := T) +1 -1 = +0 := by
-    unfold Subst.compose; simp
-    unfold Subst.id; rfl
-
-  @[grind =]
-  theorem Ren.to_lift [RenMap T] {r : Ren} {k} : (r.lift k).to = (@Ren.to T r).lift k := by
-    cases r; simp [Ren.lift, Ren.to, Subst.lift]; case _ act =>
-    funext; case _ x =>
-    cases x
-    case zero => grind
-    case _ n => cases Nat.decLt (n + 1) k <;> simp [ite]
-
-  macro:max t:term noWs "[" σ:term "]" : term => `(smap1 $σ $t)
-  macro:max t:term noWs "[" σ:term ":" T:term "]" : term => `(smap (T := $T) $σ $t)
-  infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons
-  infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose
-  infixr:85 " ◾ " => Subst.hcompose
-
-  @[app_unexpander smap1]
-  def unexpandSubstApply1 : Lean.PrettyPrinter.Unexpander
-  | `($_ $σ $t) => `($t[$σ])
-  | _ => throw ()
-
-  @[app_unexpander smap]
-  def unexpandSubstApply : Lean.PrettyPrinter.Unexpander
-  | `($_ $σ $t) => `($t[$σ : _])
-  | `($_ (T := $T) $σ $t) => `($t[$σ : $T])
-  | _ => throw ()
-
-  @[simp, grind =]
-  theorem Ren.to_compose {r1 r2 : Ren} [RenMap T] [SubstMap T T]
-    : Ren.to (T := T) (r1 ∘ r2) = Subst.compose r1 r2
-  := by
-    funext; case _ x =>
-    cases x <;> simp [Ren.to, Subst.compose, Ren.compose]
-
-  @[simp]
-  theorem Subst.cons_head_action {t} {σ : Subst T} : (t::σ).act 0 = t := by simp [Subst.cons]
-
-  @[simp]
-  theorem Subst.cons_tail_action {t i} {σ : Subst T} : (t::σ).act (i + 1) = σ.act i := by simp [Subst.cons]
-
-end LeanSubst
diff --git a/LeanSubst/Types/List.lean b/LeanSubst/Types/List.lean
new file mode 100644
index 0000000..17ea6d8
--- /dev/null
+++ b/LeanSubst/Types/List.lean
@@ -0,0 +1,51 @@
+
+import LeanSubst.Laws
+
+namespace LeanSubst
+
+universe u1 u2 u3
+variable {S : Type u1} {T : Type u2} {U : Type u3}
+
+def List.rmap [RenMap S T] (r : Ren T) : List S -> List S
+| [] => []
+| .cons x xs => x⟨r⟩ :: rmap r xs
+
+instance [RenMap S T] : RenMap (List S) T where
+  rmap := List.rmap
+
+@[simp, grind =]
+theorem List.rmap_nil [RenMap S T] {r : Ren T} : (@List.nil S)⟨r⟩ = [] := by
+  simp [RenMap.rmap, List.rmap]
+
+@[simp, grind =]
+theorem List.rmap_cons [RenMap S T] {x} {xs : List S} {r : Ren T} : (x::xs)⟨r⟩ = x⟨r⟩::xs⟨r⟩ := by
+  simp [RenMap.rmap, List.rmap]
+
+instance [RenMap S T] [RenMapId S T] : RenMapId (List S) T where
+  apply_id := by intro t; induction t <;> simp [*]
+
+instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (List S) T where
+  apply_compose := by intro s σ τ; induction s <;> simp [*]
+
+def List.smap [SubstMap S T] (σ : Subst T) : List S -> List S
+| [] => []
+| .cons x xs => x[σ] :: smap σ xs
+
+instance [SubstMap S T] : SubstMap (List S) T where
+  smap := List.smap
+
+@[simp, grind =]
+theorem List.smap_none [SubstMap S T] {σ : Subst T} : (@List.nil S)[σ] = [] := by
+  simp [SubstMap.smap, List.smap]
+
+@[simp, grind =]
+theorem List.smap_some [SubstMap S T] {x} {xs : List S} {σ : Subst T} : (x::xs)[σ] = x[σ]::xs[σ]
+:= by simp [SubstMap.smap, List.smap]
+
+instance [RenMap S T] [SubstMap S T] [SubstMapId S T] : SubstMapId (List S) T where
+  apply_id := by intro t; induction t <;> simp [*]
+
+instance [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] : SubstMapCompose (List S) T where
+  apply_compose := by intro s σ τ; induction s <;> simp [*]
+
+end LeanSubst
diff --git a/LeanSubst/Types/Option.lean b/LeanSubst/Types/Option.lean
new file mode 100644
index 0000000..ac46d4f
--- /dev/null
+++ b/LeanSubst/Types/Option.lean
@@ -0,0 +1,51 @@
+
+import LeanSubst.Laws
+
+namespace LeanSubst
+
+universe u1 u2 u3
+variable {S : Type u1} {T : Type u2} {U : Type u3}
+
+def Option.rmap [i : RenMap S T] (r : Ren T) : Option S -> Option S
+| none => none
+| some t => some t⟨r⟩
+
+instance [RenMap S T] : RenMap (Option S) T where
+  rmap := Option.rmap
+
+@[simp, grind =]
+theorem Option.rmap_none [RenMap S T] {r : Ren T} : (@Option.none S)⟨r⟩ = none := by
+  simp [RenMap.rmap, Option.rmap]
+
+@[simp, grind =]
+theorem Option.rmap_some [RenMap S T] {x : S} {r : Ren T} : (some x)⟨r⟩ = some x⟨r⟩ := by
+  simp [RenMap.rmap, Option.rmap]
+
+instance [RenMap S T] [RenMapId S T] : RenMapId (Option S) T where
+  apply_id := by intro t; cases t <;> simp
+
+instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (Option S) T where
+  apply_compose := by intro s σ τ; cases s <;> simp
+
+def Option.smap [SubstMap S T] (σ : Subst T) : Option S -> Option S
+| none => none
+| some t => some t[σ]
+
+instance [SubstMap S T] : SubstMap (Option S) T where
+  smap := Option.smap
+
+@[simp, grind =]
+theorem Option.smap_none [SubstMap S T] {σ : Subst T} : (@Option.none S)[σ] = none := by
+  simp [SubstMap.smap, Option.smap]
+
+@[simp, grind =]
+theorem Option.smap_some [SubstMap S T] {x : S} {σ : Subst T} : (some x)[σ] = some x[σ] := by
+  simp [SubstMap.smap, Option.smap]
+
+instance [RenMap S T] [SubstMap S T] [SubstMapId S T] : SubstMapId (Option S) T where
+  apply_id := by intro t; cases t <;> simp
+
+instance [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] : SubstMapCompose (Option S) T where
+  apply_compose := by intro s σ τ; cases s <;> simp
+
+end LeanSubst