diff --git a/Algebrainet/EqN.lean b/Algebrainet/Eqv.lean
similarity index 53%
rename from Algebrainet/EqN.lean
rename to Algebrainet/Eqv.lean
index be9918a..995bb93 100644
--- a/Algebrainet/EqN.lean
+++ b/Algebrainet/Eqv.lean
@@ -2,44 +2,44 @@ import Algebrainet.Net
 
 open Net
 
-inductive EqA (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
+inductive EqvA (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
   | mix_nil :
     {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
-    EqA S # (mix x nil) x
+    EqvA S # (mix x nil) x
   | nil_mix :
     {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
-    EqA S # (mix nil x) x
+    EqvA S # (mix nil x) x
   | mix_assoc :
     {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
     {yᵢ yₒ : Nat} -> {y : Net S yᵢ yₒ} ->
     {zᵢ zₒ : Nat} -> {z : Net S zᵢ zₒ} ->
-    EqA S # (mix (mix x y) z) (mix x (mix y z))
+    EqvA S # (mix (mix x y) z) (mix x (mix y z))
 
   | cat_wires :
     {xᵢ xₒ n : Nat} -> {x : Net S xᵢ xₒ} ->
     {h : _} ->
-    EqA S # (cat h x (wires n)) x
+    EqvA S # (cat h x (wires n)) x
   | wires_cat :
     {xᵢ xₒ n : Nat} -> {x : Net S xᵢ xₒ} ->
     {h : _} ->
-    EqA S # (cat h (wires n) x) x
+    EqvA S # (cat h (wires n) x) x
   | cat_assoc :
     {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
     {yᵢ yₒ : Nat} -> {y : Net S yᵢ yₒ} ->
     {zᵢ zₒ : Nat} -> {z : Net S zᵢ zₒ} ->
     {h₀ h₁ h₂ h₃ : _} ->
-    EqA S # (cat h₀ (cat h₁ x y) z) (cat h₂ x (cat h₃ y z))
+    EqvA S # (cat h₀ (cat h₁ x y) z) (cat h₂ x (cat h₃ y z))
 
-  | swap_swap : EqA S # (cat # swap swap) (mix wire wire)
-  | cup_swap : EqA S # (cat # cup swap) cup
-  | swap_cap : EqA S # (cat # swap cap) cap
+  | swap_swap : EqvA S # (cat # swap swap) (mix wire wire)
+  | cup_swap : EqvA S # (cat # cup swap) cup
+  | swap_cap : EqvA S # (cat # swap cap) cap
 
-  | move_cup : EqA S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire))
-  | move_cap : EqA S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap))
-  | move_swap : EqA S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire)))
-  | move_agent {A : S.Agent} : EqA S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A)))
+  | move_cup : EqvA S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire))
+  | move_cap : EqvA S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap))
+  | move_swap : EqvA S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire)))
+  | move_agent {A : S.Agent} : EqvA S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A)))
 
-  | cup_cap : EqA S # (cat # (mix cup wire) (mix wire cap)) wire
+  | cup_cap : EqvA S # (cat # (mix cup wire) (mix wire cap)) wire
 
   | exch :
     {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} ->
@@ -47,56 +47,56 @@ inductive EqA (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) 
     {zᵢ zₒ : Nat} -> {z : Net S zᵢ zₒ} ->
     {wᵢ wₒ : Nat} -> {w : Net S wᵢ wₒ} ->
     {h₀ h₁ h₂ : _} ->
-    EqA S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w))
+    EqvA S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w))
 
   | cat₀ :
     {aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
     {bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
     {cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
     {h₀ h₁ h₂ : _} ->
-    EqA S h₀ a b ->
-    EqA S # (cat h₁ a c) (cat h₂ b c)
+    EqvA S h₀ a b ->
+    EqvA S # (cat h₁ a c) (cat h₂ b c)
 
   | cat₁ :
     {aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
     {bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
     {cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
     {h₀ h₁ h₂ : _} ->
-    EqA S h₀ a b ->
-    EqA S # (cat h₁ c a) (cat h₂ c b)
+    EqvA S h₀ a b ->
+    EqvA S # (cat h₁ c a) (cat h₂ c b)
 
   | mix₀ :
     {aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
     {bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
     {cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
     {h : _} ->
-    EqA S h a b ->
-    EqA S # (mix a c) (mix b c)
+    EqvA S h a b ->
+    EqvA S # (mix a c) (mix b c)
 
   | mix₁ :
     {aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
     {bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
     {cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
     {h : _} ->
-    EqA S h a b ->
-    EqA S # (mix c a) (mix c b)
+    EqvA S h a b ->
+    EqvA S # (mix c a) (mix c b)
 
-inductive EqN (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
-  | refl : {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} -> EqN S # x x
+inductive Eqv (S : System) : {i₁ o₁ i₂ o₂ : Nat} -> (h : (i₁ = i₂) ∧ (o₁ = o₂)) -> (x : Net S i₁ o₁) -> (y : Net S i₂ o₂) -> Prop
+  | refl : {xᵢ xₒ : Nat} -> {x : Net S xᵢ xₒ} -> Eqv S # x x
   | fw :
     {aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
     {bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
     {cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
-    {h₀ h₁ : _} -> EqA S h₀ a b -> EqN S h₁ b c ->
-    EqN S # a c
+    {h₀ h₁ : _} -> EqvA S h₀ a b -> Eqv S h₁ b c ->
+    Eqv S # a c
   | bk :
     {aᵢ aₒ : Nat} -> {a : Net S aᵢ aₒ} ->
     {bᵢ bₒ : Nat} -> {b : Net S bᵢ bₒ} ->
     {cᵢ cₒ : Nat} -> {c : Net S cᵢ cₒ} ->
-    {h₀ h₁ : _} -> EqA S h₀ b a -> EqN S h₁ b c ->
-    EqN S (by rcases h₀ with ⟨⟨⟩,⟨⟩⟩; simp [*]) a c
+    {h₀ h₁ : _} -> EqvA S h₀ b a -> Eqv S h₁ b c ->
+    Eqv S (by rcases h₀ with ⟨⟨⟩,⟨⟩⟩; simp [*]) a c
 
-namespace EqN
+namespace Eqv
 
 variable
   {S : System}
@@ -107,68 +107,68 @@ variable
   {n : Nat}
 
 def cast_ {i₁ o₁ i₂ o₂ : Nat} {x : Net S i₁ o₁} :
-  {h : (i₁ = i₂) ∧ (o₁ = o₂)} -> EqN S # (castₙ h x) x
+  {h : (i₁ = i₂) ∧ (o₁ = o₂)} -> Eqv S # (castₙ h x) x
   | (And.intro rfl rfl) => refl
 
-def trans {h₀ h₁ : _} (e : EqN S h₀ a b) (f : EqN S h₁ b c) : EqN S # a c := by
+def trans {h₀ h₁ : _} (e : Eqv S h₀ a b) (f : Eqv S h₁ b c) : Eqv S # a c := by
   induction e with
   | refl => exact f
   | fw a _ ih => exact fw a (ih f)
   | bk a _ ih => exact bk a (ih f)
 
-def symm {h : _} (e : EqN S h a b) : EqN S # b a := by
+def symm {h : _} (e : Eqv S h a b) : Eqv S # b a := by
   induction e with
   | refl => exact refl
   | fw a _ ih => exact trans ih (bk a refl)
   | bk a _ ih => exact trans ih (fw a refl)
 
-def cat₀ {h₀ : _} (e : EqN S h₀ a b) {h₁ h₂ : _} : EqN S # (cat h₁ a c) (cat h₂ b c) := by
+def cat₀ {h₀ : _} (e : Eqv S h₀ a b) {h₁ h₂ : _} : Eqv S # (cat h₁ a c) (cat h₂ b c) := by
   induction e with
   | refl => exact refl
   | fw a _ ih => exact fw (b := (cat # _ _)) (.cat₀ a) ih
   | bk a _ ih => exact bk (b := (cat # _ _)) (.cat₀ a) ih
 
-def cat₁ {h₀ : _} (e : EqN S h₀ a b) {h₁ h₂ : _} : EqN S # (cat h₁ c a) (cat h₂ c b) := by
+def cat₁ {h₀ : _} (e : Eqv S h₀ a b) {h₁ h₂ : _} : Eqv S # (cat h₁ c a) (cat h₂ c b) := by
   induction e with
   | refl => exact refl
   | fw a _ ih => exact fw (b := (cat # _ _)) (.cat₁ a) ih
   | bk a _ ih => exact bk (b := (cat # _ _)) (.cat₁ a) ih
 
-def mix₀ {h : _} (e : EqN S h a b) : EqN S # (mix a c) (mix b c) := by
+def mix₀ {h : _} (e : Eqv S h a b) : Eqv S # (mix a c) (mix b c) := by
   induction e with
   | refl => exact refl
   | fw a _ ih => exact fw (.mix₀ a) ih
   | bk a _ ih => exact bk (.mix₀ a) ih
 
-def mix₁ {h : _} (e : EqN S h a b) : EqN S # (mix c a) (mix c b) := by
+def mix₁ {h : _} (e : Eqv S h a b) : Eqv S # (mix c a) (mix c b) := by
   induction e with
   | refl => exact refl
   | fw a _ ih => exact fw (.mix₁ a) ih
   | bk a _ ih => exact bk (.mix₁ a) ih
 
-def cat_ {h₀ h₁ : _} (e : EqN S h₀ a b) (f : EqN S h₁ c d) {h₁ h₂ : _} : EqN S # (cat h₁ a c) (cat h₂ b d) := by
+def cat_ {h₀ h₁ : _} (e : Eqv S h₀ a b) (f : Eqv S h₁ c d) {h₁ h₂ : _} : Eqv S # (cat h₁ a c) (cat h₂ b d) := by
   apply trans (cat₀ e) (cat₁ f); simp [*]
 
-def mix_ {h₀ h₁ : _} (e : EqN S h₀ a b) (f : EqN S h₁ c d) : EqN S # (mix a c) (mix b d) :=
+def mix_ {h₀ h₁ : _} (e : Eqv S h₀ a b) (f : Eqv S h₁ c d) : Eqv S # (mix a c) (mix b d) :=
   trans (mix₀ e) (mix₁ f)
 
-def mix_nil : EqN S # (mix a nil) a := fw .mix_nil refl
-def nil_mix : EqN S # (mix nil a) a := fw .nil_mix refl
-def mix_assoc : EqN S # (mix (mix a b) c) (mix a (mix b c)) := fw .mix_assoc refl
+def mix_nil : Eqv S # (mix a nil) a := fw .mix_nil refl
+def nil_mix : Eqv S # (mix nil a) a := fw .nil_mix refl
+def mix_assoc : Eqv S # (mix (mix a b) c) (mix a (mix b c)) := fw .mix_assoc refl
 
-def cat_wires {h : _} : EqN S # (cat h a (wires n)) a := fw .cat_wires refl
-def wires_cat {h : _} : EqN S # (cat h (wires n) a) a := fw .wires_cat refl
-def cat_assoc {h₀ h₁ h₂ h₃ : _} : EqN S # (cat h₀ (cat h₁ a b) c) (cat h₂ a (cat h₃ b c)) := fw .cat_assoc refl
+def cat_wires {h : _} : Eqv S # (cat h a (wires n)) a := fw .cat_wires refl
+def wires_cat {h : _} : Eqv S # (cat h (wires n) a) a := fw .wires_cat refl
+def cat_assoc {h₀ h₁ h₂ h₃ : _} : Eqv S # (cat h₀ (cat h₁ a b) c) (cat h₂ a (cat h₃ b c)) := fw .cat_assoc refl
 
-def swap_swap : EqN S # (cat # swap swap) (mix wire wire) := fw .swap_swap refl
-def cup_swap : EqN S # (cat # cup swap) cup := fw .cup_swap refl
-def swap_cap : EqN S # (cat # swap cap) cap := fw .swap_cap refl
+def swap_swap : Eqv S # (cat # swap swap) (mix wire wire) := fw .swap_swap refl
+def cup_swap : Eqv S # (cat # cup swap) cup := fw .cup_swap refl
+def swap_cap : Eqv S # (cat # swap cap) cap := fw .swap_cap refl
 
-def move_cup : EqN S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire)) := fw .move_cup refl
-def move_cap : EqN S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap)) := fw .move_cap refl
-def move_swap : EqN S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire))) := fw .move_swap refl
-def move_agent {A : S.Agent} : EqN S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A))) := fw .move_agent refl
+def move_cup : Eqv S # (cat # (mix cup wire) (mix wire swap)) (cat # (mix wire cup) (mix swap wire)) := fw .move_cup refl
+def move_cap : Eqv S # (cat # (mix wire swap) (mix cap wire)) (cat # (mix swap wire) (mix wire cap)) := fw .move_cap refl
+def move_swap : Eqv S # (cat # (mix wire swap) (cat # (mix swap wire) (mix wire swap))) (cat # (mix swap wire) (cat # (mix wire swap) (mix swap wire))) := fw .move_swap refl
+def move_agent {A : S.Agent} : Eqv S # (cat # ((agent A).mix wire) swap) (cat # (twist (S.arity A) 1) (wire.mix (agent A))) := fw .move_agent refl
 
-def cup_cap : EqN S # (cat # (mix cup wire) (mix wire cap)) wire := fw .cup_cap refl
+def cup_cap : Eqv S # (cat # (mix cup wire) (mix wire cap)) wire := fw .cup_cap refl
 
-def exch {h₀ h₁ h₂ : _} : EqN S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w)) := fw .exch refl
+def exch {h₀ h₁ h₂ : _} : Eqv S # (cat h₀ (mix x y) (mix z w)) (mix (cat h₁ x z) (cat h₂ y w)) := fw .exch refl
diff --git a/Algebrainet/EqN/Move.lean b/Algebrainet/Eqv/Move.lean
similarity index 97%
rename from Algebrainet/EqN/Move.lean
rename to Algebrainet/Eqv/Move.lean
index 554e217..5adb113 100644
--- a/Algebrainet/EqN/Move.lean
+++ b/Algebrainet/Eqv/Move.lean
@@ -1,8 +1,8 @@
 import Algebrainet.Net
-import Algebrainet.EqN.Twist
+import Algebrainet.Eqv.Twist
 
 open Net
-namespace EqN
+namespace Eqv
 
 variable {S : System}
 
@@ -11,7 +11,7 @@ set_option autoImplicit false
 def twist_net_wire
   {aᵢ aₒ: Nat}
   {A : Net S aᵢ aₒ}
-: EqN S #
+: Eqv S #
   (cat # (mix A wire) (twist aₒ 1))
   (cat # (twist aᵢ 1) (mix wire A))
 := by
@@ -154,7 +154,7 @@ def twist_net_wire
 def twist_net_wires
   {aᵢ aₒ b : Nat}
   {A : Net S aᵢ aₒ}
-: EqN S #
+: Eqv S #
   (cat # (mix A (wires b)) (twist aₒ b))
   (cat # (twist aᵢ b) (mix (wires b) A))
 := by
@@ -191,7 +191,7 @@ def twist_net_wires
 
 def twist_wires_net
   {a bᵢ bₒ : Nat} {B : Net S bᵢ bₒ}
-  : EqN S #
+  : Eqv S #
     (cat # (mix (wires a) B) (twist a bₒ))
     (cat # (twist a bᵢ) (mix B (wires a)))
 := by
@@ -213,7 +213,7 @@ def twist_wires_net
 def twist_nets
   {aᵢ aₒ : Nat} {A : Net S aᵢ aₒ}
   {bᵢ bₒ : Nat} {B : Net S bᵢ bₒ}
-  : EqN S #
+  : Eqv S #
     (cat # (mix A B) (twist aₒ bₒ))
     (cat # (twist aᵢ bᵢ) (mix B A))
 := by
@@ -227,7 +227,7 @@ def twist_nets
   apply cat₁ (symm down_up)
   repeat simp
 
-def cap_cup : EqN S # (cat # (mix wire cup) (mix cap wire)) wire := by
+def cap_cup : Eqv S # (cat # (mix wire cup) (mix cap wire)) wire := by
   apply trans; apply cat₀; .
     apply trans (mix_ wire_cat.symm cup_swap.symm)
     apply exch.symm
diff --git a/Algebrainet/EqN/Twist.lean b/Algebrainet/Eqv/Twist.lean
similarity index 89%
rename from Algebrainet/EqN/Twist.lean
rename to Algebrainet/Eqv/Twist.lean
index 42619d8..16b1b93 100644
--- a/Algebrainet/EqN/Twist.lean
+++ b/Algebrainet/Eqv/Twist.lean
@@ -1,13 +1,13 @@
-import Algebrainet.EqN
-import Algebrainet.EqN.Wires
+import Algebrainet.Eqv
+import Algebrainet.Eqv.Wires
 
-namespace EqN
+namespace Eqv
 open Net
 
 variable {S : System} {n a b : Nat}
 set_option autoImplicit false
 
-def twist₁_1 : EqN S # (twist₁ 1) swap := by
+def twist₁_1 : Eqv S # (twist₁ 1) swap := by
   apply trans cast_
   apply trans; apply cat_
   . apply wires₂.symm
@@ -15,7 +15,7 @@ def twist₁_1 : EqN S # (twist₁ 1) swap := by
   simp
   apply wires_cat
 
-def twist_1_n : EqN S # (twist 1 n) (twist₁ n) := by
+def twist_1_n : Eqv S # (twist 1 n) (twist₁ n) := by
   apply trans cast_
   apply trans; apply cat_
   . apply trans (mix₁ cast_) wire_mix_wires
@@ -23,9 +23,9 @@ def twist_1_n : EqN S # (twist 1 n) (twist₁ n) := by
   simp
   apply wires_cat
 
-def twist_1_1 : EqN S # (twist 1 1) swap := trans twist_1_n twist₁_1
+def twist_1_1 : Eqv S # (twist 1 1) swap := trans twist_1_n twist₁_1
 
-def twist₁_succ : EqN S # (twist₁ (n + 1)) (cat # (mix swap (wires n)) (mix wire (twist₁ n))) := by
+def twist₁_succ : Eqv S # (twist₁ (n + 1)) (cat # (mix swap (wires n)) (mix wire (twist₁ n))) := by
   induction n with
   | zero =>
     apply trans twist₁_1
@@ -58,7 +58,7 @@ def twist₁_succ : EqN S # (twist₁ (n + 1)) (cat # (mix swap (wires n)) (mix
 
 abbrev untwist₁ (n : Nat) : Net S (n + 1) (1 + n) := twist n 1
 
-def untwist₁_succ : EqN S # (untwist₁ (n + 1)) (cat # (mix (wires n) swap) (mix (untwist₁ n) wire)) := by
+def untwist₁_succ : Eqv S # (untwist₁ (n + 1)) (cat # (mix (wires n) swap) (mix (untwist₁ n) wire)) := by
   induction n with
   | zero =>
     apply trans cast_
@@ -89,7 +89,7 @@ def untwist₁_succ : EqN S # (untwist₁ (n + 1)) (cat # (mix (wires n) swap) (
       repeat simp
     simp
 
-def twist₁_untwist₁ : EqN S # (cat # (twist₁ n) (untwist₁ n)) (wires (n + 1)) := by
+def twist₁_untwist₁ : Eqv S # (cat # (twist₁ n) (untwist₁ n)) (wires (n + 1)) := by
   induction n with
   | zero => apply trans wire_cat cast_
   | succ n ih =>
@@ -111,7 +111,7 @@ def twist₁_untwist₁ : EqN S # (cat # (twist₁ n) (untwist₁ n)) (wires (n
     apply mix_ ih wire_cat
     repeat simp
 
-def twist_n_0 : EqN S # (twist n 0) (wires n) := by
+def twist_n_0 : Eqv S # (twist n 0) (wires n) := by
   induction n with
   | zero => apply cast_
   | succ n ih =>
@@ -123,7 +123,7 @@ def twist_n_0 : EqN S # (twist n 0) (wires n) := by
     simp
     apply wires_cat
 
-def twist_s_n : EqN S # (twist (a + 1) b) (cat # (mix (wires a) (twist₁ b)) (mix (twist a b) wire)) := by
+def twist_s_n : Eqv S # (twist (a + 1) b) (cat # (mix (wires a) (twist₁ b)) (mix (twist a b) wire)) := by
   induction a with
   | zero =>
     apply trans cast_
@@ -154,7 +154,7 @@ def twist_s_n : EqN S # (twist (a + 1) b) (cat # (mix (wires a) (twist₁ b)) (m
       repeat simp
     simp
 
-def twist_n_s : EqN S # (twist a (b + 1)) (cat # (mix (twist a b) wire) (mix (wires b) (untwist₁ a))) := by
+def twist_n_s : Eqv S # (twist a (b + 1)) (cat # (mix (twist a b) wire) (mix (wires b) (untwist₁ a))) := by
   induction a with
   | zero =>
     apply trans cast_
@@ -208,7 +208,7 @@ def twist_n_s : EqN S # (twist a (b + 1)) (cat # (mix (twist a b) wire) (mix (wi
     apply mix_ cat_wires untwist₁_succ.symm
     repeat simp
 
-def twist_untwist : EqN S # (cat # (twist a b) (twist b a)) (wires (a + b)) := by
+def twist_untwist : Eqv S # (cat # (twist a b) (twist b a)) (wires (a + b)) := by
   induction a with
   | zero =>
     apply trans (cat_ cast_ twist_n_0)
@@ -232,7 +232,7 @@ def twist_untwist : EqN S # (cat # (twist a b) (twist b a)) (wires (a + b)) := b
     apply wires_mix_wires_
     repeat simp
 
-def twist_add_n : EqN S # (twist (a + b) n) (cat # (mix (wires a) (twist b n)) (mix (twist a n) (wires b))) := by
+def twist_add_n : Eqv S # (twist (a + b) n) (cat # (mix (wires a) (twist b n)) (mix (twist a n) (wires b))) := by
   induction b with
   | zero =>
     apply symm
@@ -263,7 +263,7 @@ def twist_add_n : EqN S # (twist (a + b) n) (cat # (mix (wires a) (twist b n)) (
     . apply mix_assoc
     repeat simp
 
-def twist_n_add : EqN S # (twist n (a + b)) (cat # (mix (twist n a) (wires b)) (mix (wires a) (twist n b))) := by
+def twist_n_add : Eqv S # (twist n (a + b)) (cat # (mix (twist n a) (wires b)) (mix (wires a) (twist n b))) := by
   apply trans (cat_wires (n := (a + b + n))).symm
   apply trans; apply cat₁; .
     apply trans (wires_mix_wires_ (a := a) (b := b + n)).symm
@@ -292,7 +292,7 @@ def twist_n_add : EqN S # (twist n (a + b)) (cat # (mix (twist n a) (wires b)) (
   apply wires_cat
   repeat simp
 
-def twist_2_1 : EqN S # (twist 2 1) (cat # (mix wire swap) (mix swap wire)) := by
+def twist_2_1 : Eqv S # (twist 2 1) (cat # (mix wire swap) (mix swap wire)) := by
   apply trans (twist_add_n (a := 1) (b := 1))
   apply cat_
   . apply mix_
@@ -302,7 +302,7 @@ def twist_2_1 : EqN S # (twist 2 1) (cat # (mix wire swap) (mix swap wire)) := b
     . apply twist_1_1
     . apply wires₁
 
-def twist_1_2 : EqN S # (twist 1 2) (cat # (mix swap wire) (mix wire swap)) := by
+def twist_1_2 : Eqv S # (twist 1 2) (cat # (mix swap wire) (mix wire swap)) := by
   apply trans (twist_n_add (a := 1) (b := 1))
   apply cat_
   . apply mix_
diff --git a/Algebrainet/EqN/Wires.lean b/Algebrainet/Eqv/Wires.lean
similarity index 57%
rename from Algebrainet/EqN/Wires.lean
rename to Algebrainet/Eqv/Wires.lean
index b11b9a2..693b167 100644
--- a/Algebrainet/EqN/Wires.lean
+++ b/Algebrainet/Eqv/Wires.lean
@@ -1,6 +1,6 @@
-import Algebrainet.EqN
+import Algebrainet.Eqv
 
-namespace EqN
+namespace Eqv
 open Net
 
 variable
@@ -11,14 +11,14 @@ variable
 
 set_option autoImplicit false
 
-def wires₁ : EqN S # (wires 1) wire := nil_mix
-def wires₂ : EqN S # (wires 2) (mix wire wire) := mix₀ wires₁
-def cat_wire {h : _} : EqN S # (cat h A wire) A := trans (cat₁ (h₂ := h) (symm wires₁)) (cat_wires)
-def wire_cat {h : _} : EqN S # (cat h wire A) A := trans (cat₀ (h₂ := h) (symm wires₁)) (wires_cat)
-def wires_ : {h : n₁ = n₂} -> EqN S # (wires n₁) (wires n₂)
+def wires₁ : Eqv S # (wires 1) wire := nil_mix
+def wires₂ : Eqv S # (wires 2) (mix wire wire) := mix₀ wires₁
+def cat_wire {h : _} : Eqv S # (cat h A wire) A := trans (cat₁ (h₂ := h) (symm wires₁)) (cat_wires)
+def wire_cat {h : _} : Eqv S # (cat h wire A) A := trans (cat₀ (h₂ := h) (symm wires₁)) (wires_cat)
+def wires_ : {h : n₁ = n₂} -> Eqv S # (wires n₁) (wires n₂)
   | rfl => refl
 
-def wires_mix_wires_ {h : a + b = n} : EqN S # (mix (wires a) (wires b)) (wires n) := by
+def wires_mix_wires_ {h : a + b = n} : Eqv S # (mix (wires a) (wires b)) (wires n) := by
   induction b generalizing n with
   | zero => subst h; apply mix_nil
   | succ b ih =>
@@ -27,23 +27,23 @@ def wires_mix_wires_ {h : a + b = n} : EqN S # (mix (wires a) (wires b)) (wires
     apply wires_
     repeat simp [*]
 
-def wires_mix_wires : EqN S # (mix (wires a) (wires b)) (wires (a + b)) := by apply wires_mix_wires_; rfl
+def wires_mix_wires : Eqv S # (mix (wires a) (wires b)) (wires (a + b)) := by apply wires_mix_wires_; rfl
 
-def wire_mix_wires_ {h : a + 1 = n} : EqN S # (mix wire (wires a)) (wires n) := by
+def wire_mix_wires_ {h : a + 1 = n} : Eqv S # (mix wire (wires a)) (wires n) := by
   apply trans (mix₀ wires₁.symm)
   apply wires_mix_wires_
   simp [*]
 
-def wire_mix_wires : EqN S # (mix wire (wires a)) (wires (a + 1)) := by apply wire_mix_wires_; rfl
+def wire_mix_wires : Eqv S # (mix wire (wires a)) (wires (a + 1)) := by apply wire_mix_wires_; rfl
 
-def up_down : EqN S # (mix A B) (cat # (mix (wires aᵢ) B) (mix A (wires bₒ))) := by
+def up_down : Eqv S # (mix A B) (cat # (mix (wires aᵢ) B) (mix A (wires bₒ))) := by
   apply trans
   apply mix_
   apply symm (wires_cat (n := aᵢ)); simp
   apply symm (cat_wires (n := bₒ)); simp
   apply symm exch
 
-def down_up : EqN S # (mix A B) (cat # (mix A (wires bᵢ)) (mix (wires aₒ) B)) := by
+def down_up : Eqv S # (mix A B) (cat # (mix A (wires bᵢ)) (mix (wires aₒ) B)) := by
   apply trans
   apply mix_
   apply symm (cat_wires (n := aₒ)); simp
diff --git a/Algebrainet/Rd.lean b/Algebrainet/Rd.lean
index 561fea5..b2f25aa 100644
--- a/Algebrainet/Rd.lean
+++ b/Algebrainet/Rd.lean
@@ -1,5 +1,5 @@
 import Algebrainet.Net
-import Algebrainet.EqN
+import Algebrainet.Eqv
 
 open Net
 
@@ -9,7 +9,7 @@ structure Rules (S : System) where
   defined : S.Agent -> S.Agent -> Prop
   defined_symm : {a b : S.Agent} -> defined a b -> defined b a
   rule : {a b : S.Agent} -> defined a b -> Net S ((S.arity a) + (S.arity b)) 0
-  rule_symm : {a b : S.Agent} -> (d : defined a b) -> EqN S # (rule d) (rule (defined_symm d))
+  rule_symm : {a b : S.Agent} -> (d : defined a b) -> Eqv S # (rule d) (rule (defined_symm d))
 
 def pair {S : System} (a b : S.Agent) : Net S ((S.arity a) + (S.arity b)) 0 :=
   cat # (mix (agent a) (agent b)) cap
@@ -45,38 +45,34 @@ inductive Vee (R : Rules S) {i o : Nat} (b c : Net S i o) : Prop
   | eq : (b = c) -> Vee R b c
   | rd : {d : Net S i o} -> Rd S R b d -> Rd S R c d -> Vee R b c
 
-abbrev NEq {S : System} {aᵢ aₒ bᵢ bₒ : Nat} (a : Net S aᵢ aₒ) (b : Net S bᵢ bₒ) : Prop
+abbrev EqN {S : System} {aᵢ aₒ bᵢ bₒ : Nat} (a : Net S aᵢ aₒ) (b : Net S bᵢ bₒ) : Prop
   := Eq (α := Σ i o, Net S i o) ⟨aᵢ, aₒ, a⟩ ⟨bᵢ, bₒ, b⟩
 
 def extract_agent {i o : Nat} : (n : Net S i o) -> Option S.Agent
   | agent a => some a
   | _ => none
 
-namespace NEq
+namespace EqN
 
 variable
   {aᵢ aₒ bᵢ bₒ : Nat} {a : Net S aᵢ aₒ} {b : Net S bᵢ bₒ}
 
 def congr
   {α : Type}
-  (h : NEq a b)
+  (h : EqN a b)
   (f : {i o : Nat} -> Net S i o -> α)
   : f a = f b
 := Eq.rec (motive := fun b _ => f a = f b.snd.snd) rfl h
 
-@[simp] def eqᵢ (h : NEq a b) : aᵢ = bᵢ := Eq.rec (motive := fun b _ => aᵢ = b.fst) rfl h
-@[simp] def eqₒ (h : NEq a b) : aₒ = bₒ := Eq.rec (motive := fun b _ => aₒ = b.snd.fst) rfl h
+@[simp] def eqᵢ (h : EqN a b) : aᵢ = bᵢ := Eq.rec (motive := fun b _ => aᵢ = b.fst) rfl h
+@[simp] def eqₒ (h : EqN a b) : aₒ = bₒ := Eq.rec (motive := fun b _ => aₒ = b.snd.fst) rfl h
 
-end NEq
-
-def extract_pair {i o : Nat} : (n : Net S i o) -> Option (S.Agent × S.Agent)
-  | cat _ (mix (agent a) (agent b)) cap => some (a, b)
-  | _ => none
+end EqN
 
 abbrev SNet (S : System) := Σ i o, Net S i o
 
-def extract_cat {i o : Nat} : (n : Net S i o) -> Option (SNet S × SNet S)
-  | cat _ a b => some (⟨_, _, a⟩, ⟨_, _, b⟩)
+def unpair {i o : Nat} : (n : Net S i o) -> Option (S.Agent × S.Agent)
+  | cat _ (mix (agent a) (agent b)) cap => some (a, b)
   | _ => none
 
 def uncat₀ {i o : Nat} : (n : Net S i o) -> Option (SNet S)
@@ -127,14 +123,14 @@ def rd_perf_conf_ {S : System} {R : Rules S}
   {i₀ o₀ i₁ o₁ : Nat}
   {a₀ b : Net S i₀ o₀} {a₁ c : Net S i₁ o₁}
   (r₀ : Rd S R a₀ b) (r₁ : Rd S R a₁ c)
-  (hₐ : NEq a₀ a₁)
+  (hₐ : EqN a₀ a₁)
   : Vee R (castₙ ⟨hₐ.eqᵢ, hₐ.eqₒ⟩ b) c
 := by
   induction r₀ generalizing i₁ o₁ a₁ c r₁ with
   | pair x₀ y₀ d₀ =>
     cases r₁ with
     | pair x₁ y₁ d₁ =>
-      cases hₐ.congr extract_pair
+      cases hₐ.congr unpair
       apply Vee.eq
       simp
     | mix₀ | mix₁ => repeat cases hₐ.congr kind