diff --git a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean
index 6944ee7..bd74cce 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean
@@ -1,8 +1,8 @@
-import Discretion.Wk.List
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions
 import DeBruijnSSA.BinSyntax.Typing.Ty
+import DeBruijnSSA.ListWk
 
 namespace BinSyntax
 
@@ -513,7 +513,7 @@ theorem mem_wk {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ ρ) (hV : V
   ⟨V', hV', hn' ▸ hV⟩
 
 -- theorem EWkn.id_len_le : Γ.EWkn Δ _root_.id → Δ.length ≤ Γ.length := by
---   apply List.IsWk.id_len_le
+--   apply List.NEWkn.id_len_le
 
 theorem Var.wk_res (h : V ≤ V') (hΓ : Γ.Var n V) : Γ.Var n V' where
   length := hΓ.length
@@ -537,7 +537,7 @@ end Basic
 section EWkn
 
 def EWkn (Γ Δ : Ctx α ε) (ρ : ℕ → ℕ) : Prop -- TODO: fin argument as defeq?
-  := List.IsWk Γ Δ ρ
+  := List.NEWkn Γ Δ ρ
 
 theorem EWkn.wkn [PartialOrder α] [PartialOrder ε]
   {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.EWkn Δ ρ) : Γ.Wkn Δ ρ := Wkn_iff.mpr h.toNWkn
@@ -549,17 +549,17 @@ theorem EWkn.var_inv [PartialOrder α] [PartialOrder ε] {Γ Δ : Ctx α ε} {ρ
   (hi : i < Δ.length) (hv : Γ.Var (ρ i) V) : Δ.Var i V := ⟨hi, have ⟨_, he⟩ := h i hi; he ▸ hv.get⟩
 
 @[simp]
-theorem EWkn.id {Γ : Ctx α ε} : Γ.EWkn Γ id := List.IsWk.id _
+theorem EWkn.id {Γ : Ctx α ε} : Γ.EWkn Γ id := List.NEWkn.id _
 
 theorem EWkn.lift {Γ Δ : Ctx α ε} {V : Ty α × ε} (h : Γ.EWkn Δ ρ)
   : EWkn (V::Γ) (V::Δ) (Nat.liftWk ρ)
-  := List.IsWk.lift h
+  := List.NEWkn.lift h
 
 theorem EWkn.lift_tail {left right : Ty α × ε} (h : EWkn (left::Γ) (right::Δ) (Nat.liftWk ρ))
-  : EWkn Γ Δ ρ := List.IsWk.lift_tail h
+  : EWkn Γ Δ ρ := List.NEWkn.lift_tail h
 
 theorem EWkn.lift_head {left right : Ty α × ε} (h : EWkn (left::Γ) (right::Δ) (Nat.liftWk ρ))
-  : left = right := List.IsWk.lift_head h
+  : left = right := List.NEWkn.lift_head h
 
 @[simp]
 theorem EWkn.lift_iff {left right : Ty α × ε} {Γ Δ}
@@ -582,20 +582,20 @@ theorem EWkn.lift_id_iff {left right : Ty α × ε} {Γ Δ}
     := ⟨λh => ⟨h.lift_id_head, h.lift_id_tail⟩, λ⟨h, h'⟩ => h ▸ h'.lift_id⟩
 
 theorem EWkn.step {Γ Δ : Ctx α ε} {head : Ty α × ε} (h : Γ.EWkn Δ ρ)
-  : EWkn (head::Γ) Δ (Nat.stepWk ρ) := List.IsWk.step _ h
+  : EWkn (head::Γ) Δ (Nat.stepWk ρ) := List.NEWkn.step _ h
 
 theorem EWkn.step_tail {head : Ty α × ε} (h : EWkn (head::Γ) Δ (Nat.stepWk ρ))
-  : EWkn Γ Δ ρ := List.IsWk.step_tail h
+  : EWkn Γ Δ ρ := List.NEWkn.step_tail h
 
 @[simp]
 theorem EWkn.step_iff {head : Ty α × ε} {Γ Δ}
   : EWkn (head::Γ) Δ (Nat.stepWk ρ) ↔ EWkn Γ Δ ρ
-  := List.IsWk.step_iff _ _ _ _
+  := List.NEWkn.step_iff _ _ _ _
 
 @[simp]
 theorem EWkn.succ_comp_iff {head : Ty α × ε} {Γ Δ}
   : EWkn (head::Γ) Δ (Nat.succ ∘ ρ) ↔ EWkn Γ Δ ρ
-  := List.IsWk.step_iff _ _ _ _
+  := List.NEWkn.step_iff _ _ _ _
 
 @[simp]
 theorem EWkn.succ {head} {Γ : Ctx α ε}
@@ -624,7 +624,7 @@ theorem EWkn.liftn_id₂ {Γ Δ : Ctx α ε} {left right : Ty α × ε} (h : Γ.
 
 theorem EWkn.liftn_append (Ξ) (h : Γ.EWkn Δ ρ)
   : EWkn (Ξ ++ Γ) (Ξ ++ Δ) (Nat.liftnWk Ξ.length ρ)
-  := List.IsWk.liftn_append _ h
+  := List.NEWkn.liftn_append _ h
 
 theorem EWkn.liftn_append' {Ξ} (hn : n = Ξ.length) (h : Γ.EWkn Δ ρ)
   : EWkn (Ξ ++ Γ) (Ξ ++ Δ) (Nat.liftnWk n ρ)
@@ -648,7 +648,7 @@ theorem EWkn.liftn_append_cons_id {Γ Δ : Ctx α ε} (A Ξ) (h : Γ.EWkn Δ _ro
 
 theorem EWkn.stepn_append (Ξ) (h : Γ.EWkn Δ ρ)
   : EWkn (Ξ ++ Γ) Δ (Nat.stepnWk Ξ.length ρ)
-  := List.IsWk.stepn_append _ h
+  := List.NEWkn.stepn_append _ h
 
 theorem EWkn.stepn_append' {Ξ} (hn : n = Ξ.length) (h : Γ.EWkn Δ ρ)
   : EWkn (Ξ ++ Γ) Δ (Nat.stepnWk n ρ)
diff --git a/DeBruijnSSA/ListWk.lean b/DeBruijnSSA/ListWk.lean
new file mode 100644
index 0000000..68c8400
--- /dev/null
+++ b/DeBruijnSSA/ListWk.lean
@@ -0,0 +1,118 @@
+import Discretion.Wk.List
+
+/-- The function `ρ` sends `Γ` to `Δ` -/
+def List.NEWkn (Γ Δ : List α) (ρ : ℕ → ℕ) : Prop
+  := ∀n, (hΔ : n < Δ.length) → ∃hΓ : ρ n < Γ.length, Γ[ρ n] = Δ[n]
+
+theorem List.NEWkn.bounded {ρ : ℕ → ℕ} (h : List.NEWkn Γ Δ ρ) (n : ℕ) (hΔ : n < Δ.length)
+  : ρ n < Γ.length := match h n hΔ with | ⟨hΓ, _⟩ => hΓ
+
+def List.NEWkn.toFinWk {ρ : ℕ → ℕ} (h : List.NEWkn Γ Δ ρ) : Fin (Δ.length) → Fin (Γ.length)
+  := Fin.wkOfBounded ρ h.bounded
+
+-- theorem List.NEWkn.toIsFWk (Γ Δ : List α) (ρ : ℕ → ℕ)
+--   (h : List.NEWkn Γ Δ ρ) : List.IsFWk Γ Δ (List.NEWkn.toFinWk h)
+--   := funext λ⟨i, hi⟩ => have ⟨_, h⟩ := h i hi; h
+
+-- ... TODO: NEWkns
+
+@[simp]
+theorem List.NEWkn.id (Γ : List α) : List.NEWkn Γ Γ id
+  := λ_ hΓ => ⟨hΓ, rfl⟩
+
+-- ... TODO: len_le
+
+@[simp]
+theorem List.NEWkn.drop_all (Γ : List α) (ρ) : List.NEWkn Γ [] ρ
+  := λi h => by cases h
+
+theorem List.NEWkn.comp {ρ : ℕ → ℕ} {σ : ℕ → ℕ} (hρ : List.NEWkn Γ Δ ρ) (hσ : List.NEWkn Δ Ξ σ)
+  : List.NEWkn Γ Ξ (ρ ∘ σ) := λn hΞ =>
+    have ⟨hΔ, hσ⟩ := hσ n hΞ;
+    have ⟨hΓ, hρ⟩ := hρ _ hΔ;
+    ⟨hΓ, hρ ▸ hσ⟩
+
+theorem List.NEWkn.lift {ρ : ℕ → ℕ} (hρ : List.NEWkn Γ Δ ρ)
+  : List.NEWkn (A :: Γ) (A :: Δ) (Nat.liftWk ρ) := λn hΔ => match n with
+  | 0 => ⟨Nat.zero_lt_succ _, rfl⟩
+  | n+1 => have ⟨hΔ, hρ⟩ := hρ n (Nat.lt_of_succ_lt_succ hΔ); ⟨Nat.succ_lt_succ hΔ, hρ⟩
+
+theorem List.NEWkn.lift_tail {ρ : ℕ → ℕ} (h : List.NEWkn (A :: Γ) (B :: Δ) (Nat.liftWk ρ))
+    : List.NEWkn Γ Δ ρ
+  := λi hΔ => have ⟨hΔ, hρ⟩ := h i.succ (Nat.succ_lt_succ hΔ); ⟨Nat.lt_of_succ_lt_succ hΔ, hρ⟩
+
+theorem List.NEWkn.lift_head {ρ : ℕ → ℕ} (h : List.NEWkn (A :: Γ) (B :: Δ) (Nat.liftWk ρ)) : A = B
+  := (h 0 (Nat.zero_lt_succ _)).2
+
+theorem List.NEWkn.lift_iff (A B) (Γ Δ : List α) (ρ : ℕ → ℕ)
+  : List.NEWkn (A :: Γ) (B :: Δ) (Nat.liftWk ρ) ↔ A = B ∧ List.NEWkn Γ Δ ρ
+  := ⟨
+    λh => ⟨h.lift_head, List.NEWkn.lift_tail h⟩,
+    λ⟨rfl, hρ⟩ => List.NEWkn.lift hρ
+  ⟩
+
+theorem List.NEWkn.lift_id (hρ : List.NEWkn Γ Δ _root_.id)
+  : List.NEWkn (A :: Γ) (A :: Δ) _root_.id := Nat.liftWk_id ▸ hρ.lift
+
+theorem List.NEWkn.lift_id_tail (h : List.NEWkn (left :: Γ) (right :: Δ) _root_.id)
+    : List.NEWkn Γ Δ _root_.id
+  := (Nat.liftWk_id ▸ h).lift_tail
+
+theorem List.NEWkn.lift_id_head (h : List.NEWkn (left :: Γ) (right :: Δ) _root_.id)
+  : left = right
+  := (Nat.liftWk_id ▸ h).lift_head
+
+theorem List.NEWkn.lift_id_iff (h : List.NEWkn (left :: Γ) (right :: Δ) _root_.id)
+  : left = right ∧ List.NEWkn Γ Δ _root_.id
+  := ⟨h.lift_id_head, h.lift_id_tail⟩
+
+theorem List.NEWkn.lift₂ {ρ : ℕ → ℕ} (hρ : List.NEWkn Γ Δ ρ)
+    : List.NEWkn (A₁ :: A₂ :: Γ) (A₁ :: A₂ :: Δ) (Nat.liftWk (Nat.liftWk ρ))
+  := hρ.lift.lift
+
+theorem List.NEWkn.liftn₂ {ρ : ℕ → ℕ} (hρ : List.NEWkn Γ Δ ρ)
+    : List.NEWkn (A₁ :: A₂ :: Γ) (A₁ :: A₂ :: Δ) (Nat.liftnWk 2 ρ)
+  := by rw [Nat.liftnWk_two]; exact hρ.lift₂
+
+theorem List.NEWkn.liftn_append {ρ : ℕ → ℕ} (Ξ : List α) (hρ : List.NEWkn Γ Δ ρ)
+    : List.NEWkn (Ξ ++ Γ) (Ξ ++ Δ) (Nat.liftnWk Ξ.length ρ) := by
+  induction Ξ with
+  | nil => exact hρ
+  | cons A Ξ I =>
+    rw [List.length, Nat.liftnWk_succ']
+    exact I.lift
+
+theorem List.NEWkn.liftn_append' {ρ : ℕ → ℕ} (Ξ : List α) (hΞ : Ξ.length = n)
+  (hρ : List.NEWkn Γ Δ ρ) : List.NEWkn (Ξ ++ Γ) (Ξ ++ Δ) (Nat.liftnWk n ρ) := hΞ ▸ hρ.liftn_append Ξ
+
+theorem List.NEWkn.step {ρ : ℕ → ℕ} (A : α) (hρ : List.NEWkn Γ Δ ρ)
+    : List.NEWkn (A :: Γ) Δ (Nat.succ ∘ ρ)
+  := λn hΔ => have ⟨hΔ, hρ⟩ := hρ n hΔ; ⟨Nat.succ_lt_succ hΔ, hρ⟩
+
+@[simp]
+theorem List.NEWkn.succ (A : α) : List.NEWkn (A :: Γ) Γ .succ := step (ρ := _root_.id) A (id _)
+
+theorem List.NEWkn.step_tail {ρ : ℕ → ℕ} (h : List.NEWkn (A :: Γ) Δ (Nat.succ ∘ ρ)) : List.NEWkn Γ Δ ρ
+  := λi hΔ => have ⟨hΔ, hρ⟩ := h i hΔ; ⟨Nat.lt_of_succ_lt_succ hΔ, hρ⟩
+
+theorem List.NEWkn.step_iff (A) (Γ Δ : List α) (ρ : ℕ → ℕ)
+  : List.NEWkn (A :: Γ) Δ (Nat.succ ∘ ρ) ↔ List.NEWkn Γ Δ ρ
+  := ⟨
+    List.NEWkn.step_tail,
+    List.NEWkn.step A
+  ⟩
+
+theorem List.NEWkn.stepn_append {ρ : ℕ → ℕ} (Ξ : List α) (hρ : List.NEWkn Γ Δ ρ)
+    : List.NEWkn (Ξ ++ Γ) Δ (Nat.stepnWk Ξ.length ρ)
+  := by induction Ξ with
+    | nil => exact hρ
+    | cons A Ξ I =>
+      rw [List.length, Nat.stepnWk_succ']
+      exact I.step _
+
+theorem List.NEWkn.stepn_append' {ρ : ℕ → ℕ} (Ξ : List α) (hΞ : Ξ.length = n)
+  (hρ : List.NEWkn Γ Δ ρ) : List.NEWkn (Ξ ++ Γ) Δ (Nat.stepnWk n ρ) := hΞ ▸ hρ.stepn_append Ξ
+
+theorem List.NEWkn.toNWkn [PartialOrder α] (Γ Δ : List α) (ρ : ℕ → ℕ)
+  (h : List.NEWkn Γ Δ ρ) : List.NWkn Γ Δ ρ
+  := λn hΔ => match h n hΔ with | ⟨hΓ, h⟩ => ⟨hΓ, le_of_eq h⟩