diff --git a/.meta/assoc_count.py b/.meta/assoc_count.py
new file mode 100755
index 0000000..a955aef
--- /dev/null
+++ b/.meta/assoc_count.py
@@ -0,0 +1,126 @@
+#!/usr/bin/env python3
+
+import re
+import os
+import sys
+import functools 
+
+
+MIN_PYTHON = (3, 10)
+if sys.version_info < MIN_PYTHON:
+  print(f"Your python version is {sys.version_info.major}.{sys.version_info.minor}. {MIN_PYTHON[0]}.{MIN_PYTHON[1]} is required")
+  exit(3)
+
+
+b_color_yellow = '\033[93m'
+b_color_cyan = '\033[96m'
+b_color_reset = '\033[0m'
+b_color_green = '\033[92m'
+b_color_red = '\033[91m'
+
+is_windows = sys.platform.startswith('win')
+if is_windows: # Disable colors on windows 
+  b_color_yellow = ''
+  b_color_cyan = ''
+  b_color_reset = ''
+  b_color_green = ''
+  b_color_red = ''
+  print("Warning: Windows detected. Disabling colored output")
+  
+curr_dir = os.path.dirname(os.path.realpath(__file__))
+src_dir = f"{curr_dir}/../src"
+
+regex_assoc : list[re.Pattern] = list(map(re.compile, [
+  r".*rewrite.*assoc",
+  r".*rewrite.*dist",
+  r".*rewrite.*mixed_product",
+  r".*rewrite.*cast",
+  r".*cleanup_zx",
+  r".*cast_id",
+  r".*simpl_cast",
+  r".*bundle_wires",
+  r".*restore_dims",
+  r".*cast_irrelevance",
+  r".*apply .*_simplify",
+  r".*rewrite.*stack_empty_.",
+  r".*rewrite.*n_stack1_",
+  r".*rewrite.*n_wire_stack",
+  r".*rewrite.*wire_to_n_wire",
+  r".*rewrite.*wire_removal_",
+  r".*rewrite.*(n_wire|nstack1)_split",
+]))
+proof_regex = re.compile(r'Proof\.((?:(?!Proof\.|Qed\.|Defined\.|Admitted\.|Abort\.)(?!\b(?:Proof|Qed|Defined|Admitted|Abort)\b)[\s\S])*?)(Qed\.|Defined\.|Admitted\.|Abort\.)')
+stmt_regex = re.compile(r'(([a-z|A-Z|0-9])+(\t| |[a-z|A-Z|0-9]|.)*)(\t| )*(\n|;|$)')
+
+class Result:
+  non_assoc : int
+  assoc : int
+  repeat_assoc : int
+
+  def __init__(self, non_assoc : int = 0, assoc : int = 0, repeat_assoc : int = 0) -> None:
+    self.non_assoc = non_assoc  
+    self.assoc = assoc
+    self.repeat_assoc = repeat_assoc
+  
+  
+  def __add__(self, other):
+    return Result(self.non_assoc + other.non_assoc, self.assoc + other.assoc, self.repeat_assoc + other.repeat_assoc)
+  
+  def __iadd__(self, other):
+    self.assoc += other.assoc
+    self.non_assoc += other.non_assoc
+    self.repeat_assoc += other.repeat_assoc
+    return self
+  
+  def total_assoc(self) -> int:
+    return self.assoc + self.repeat_assoc
+  
+  def total(self) -> int:
+    return self.total_assoc() + self.non_assoc
+    
+  def __str__(self) -> str:
+    return \
+f"""{b_color_red}Number of repeated assoc lines:{b_color_reset} {self.repeat_assoc} ({self.repeat_assoc / self.total():.2%}) ({self.repeat_assoc / self.total_assoc():.2%} of all assoc lines)
+{b_color_yellow}Number of assoc lines:{b_color_reset} {self.assoc} ({self.assoc / self.total():.2%}) ({self.assoc / self.total_assoc():.2%} of all assoc lines)
+{b_color_cyan}Total of any assoc lines:{b_color_reset} {self.total_assoc()} ({self.total_assoc() / self.total():.2%})
+{b_color_green}Number of other proof lines:{b_color_reset} {self.non_assoc} ({self.non_assoc / self.total():.2%})
+Total lines: {self.total()}
+"""
+    
+do_regex = re.compile(r'do \d+')
+  
+
+def count_assoc_non_assoc(proof : str, proof_completion : str) -> Result:
+  if proof_completion != "Qed." and proof_completion != "Defined.":
+    return Result()
+  result = Result()
+  for stmt in stmt_regex.findall(proof):
+    if any(map(lambda pattern : pattern.match(stmt[0]), regex_assoc)):
+      if 'repeat' in stmt[0] or do_regex.match(stmt[0]):
+        result.repeat_assoc += 1
+      else:
+        result.assoc += 1
+    else:
+      result.non_assoc += 1
+  return result
+
+
+def count_assoc_file(file : str) -> tuple[int, int]:
+  with open(file) as f:
+    data = f.read()
+    proofs = proof_regex.findall(data)
+    result = functools.reduce(lambda curr, proof : count_assoc_non_assoc(proof[0], proof[-1]) + curr , proofs, Result())
+    return result
+
+result = Result()
+for dir, _, files in os.walk(src_dir):
+  for file in files:
+    print(f"Checking {dir}/{file}...")
+    if not file.endswith(".v"): # Make sure we only look at Coq files
+      continue
+    result += count_assoc_file(f"{dir}/{file}")
+    
+print(result)
+  
+      
+      
diff --git a/LICENSE b/LICENSE
index 905b725..6840d31 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2021 INQWIRE
+Copyright (c) 2021 REDACTED
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
diff --git a/README.md b/README.md
index fc3c925..07aae6f 100644
--- a/README.md
+++ b/README.md
@@ -2,8 +2,6 @@
 
 Verifying the ZX Calculus
 
-[Check out the paper on arxiv](https://arxiv.org/abs/2205.05781)
-
 ## Building VyZX
 
 Works with Coq 8.16-8.18.
diff --git a/coq-vyzx.opam b/coq-vyzx.opam
index 3f1cf83..aaac4c6 100644
--- a/coq-vyzx.opam
+++ b/coq-vyzx.opam
@@ -3,17 +3,14 @@ opam-version: "2.0"
 version: "0.1.0"
 synopsis: "Coq library for reasoning about ZX diagrams"
 description: """
-inQWIRE's QuantumLib is a Coq library for reasoning
- about ZX diagrams.
+A Coq library for reasoning about ZX diagrams.
 """
-maintainer: ["inQWIRE Developers"]
-authors: ["inQWIRE"]
+maintainer: ["Anonymous"]
+authors: ["Anonymous"]
 license: "MIT"
-homepage: "https://github.com/inQWIRE/VyZX"
-bug-reports: "https://github.com/inQWIRE/VyZX/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq-quantumlib" {>= "1.3.0"}
+  "coq-quantumlib" {= "1.3.0"}
   "coq-sqir" {>= "1.3.0"}
   "coq-voqc" {>= "1.3.0"}
   "coq" {>= "8.16"}
@@ -33,4 +30,3 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/inQWIRE/VyZX.git"
diff --git a/dune-project b/dune-project
index 4415ddb..b1cfc95 100644
--- a/dune-project
+++ b/dune-project
@@ -6,19 +6,17 @@
 (generate_opam_files true)
 
 (license MIT)
-(authors "inQWIRE")
-(maintainers "inQWIRE Developers")
-(source (github inQWIRE/VyZX))
+(authors "Anonymous")
+(maintainers "Anonymous")
 
 (package
  (name coq-vyzx)
  (synopsis "Coq library for reasoning about ZX diagrams")
- (description "\| inQWIRE's QuantumLib is a Coq library for reasoning
-              "\|  about ZX diagrams.
+ (description "\| A Coq library for reasoning about ZX diagrams.
  )
 
  (depends
-   (coq-quantumlib (>= 1.3.0))
+   (coq-quantumlib (= 1.3.0))
    (coq-sqir (>= 1.3.0))
    (coq-voqc (>= 1.3.0))
    (coq (>= 8.16))))
diff --git a/src/CoreData/Proportional.v b/src/CoreData/Proportional.v
index 1a17209..1455a5c 100644
--- a/src/CoreData/Proportional.v
+++ b/src/CoreData/Proportional.v
@@ -345,6 +345,16 @@ Proof.
   assumption.
 Qed.
 
+Lemma conjugate_diagrams : forall n m (zx0 zx1 : ZX n m),
+  zx0 ⊼ ∝ zx1 ⊼ -> zx0 ∝ zx1.
+Proof.
+  intros.
+  apply adjoint_diagrams.
+  unfold adjoint.
+  rewrite H.
+  easy.
+Qed.
+
 Lemma colorswap_adjoint_commute : forall n m (zx : ZX n m),
   ⊙ (zx †) ∝ (⊙ zx) †.
 Proof.
@@ -395,11 +405,3 @@ Proof.
   apply Z_spider_1_1_fusion.
 Qed.
 
-Lemma proportional_sound : forall {nIn nOut} (zx0 zx1 : ZX nIn nOut),
-  zx0 ∝ zx1 -> exists (zxConst : ZX 0 0), ⟦ zx0 ⟧ = ⟦ zxConst ↕ zx1 ⟧.
-Proof.
-  intros.
-  simpl; unfold proportional, proportional_general in H.
-  destruct H as [c [H cneq0]].
-  rewrite H.
-Abort.
\ No newline at end of file
diff --git a/src/CoreRules/CapCupRules.v b/src/CoreRules/CapCupRules.v
index e18863a..20e2f87 100644
--- a/src/CoreRules/CapCupRules.v
+++ b/src/CoreRules/CapCupRules.v
@@ -114,15 +114,6 @@ Unshelve.
   all: lia.
 Qed.
 
-Lemma n_cup_inv_n_swap_n_wire : forall n, n_cup n ∝ n_wire n ↕ n_swap n ⟷ n_cup_unswapped n.
-Proof.
-  intros.
-  strong induction n.
-  destruct n; [ | destruct n].
-  - simpl. rewrite n_cup_0_empty. cleanup_zx. simpl_casts. easy.
-  - simpl. rewrite n_cup_1_cup. cleanup_zx. simpl_casts. bundle_wires. cleanup_zx. easy.    
-Admitted. (*TODO*)
-
 Lemma n_cup_unswapped_colorswap : forall n, ⊙ (n_cup_unswapped n) ∝ n_cup_unswapped n.
 Proof. 
   intros.
@@ -207,4 +198,72 @@ Qed.
   (fun n => @n_cap_unswapped_transpose n)
   (fun n => @n_cup_transpose n)
   (fun n => @n_cap_transpose n)
-  : transpose_db.
\ No newline at end of file
+  : transpose_db.
+Local Open Scope ZX_scope.
+
+Lemma bigyank_cap : forall (zx1 : ZX 1 1),
+  ⊂ ↕ zx1 ∝ — ↕ ⊂ ⟷ top_to_bottom 3 ⟷ (— ↕ — ↕ zx1).
+Proof.
+  intros.
+  rewrite top_to_bottom_grow_r.
+  simpl_casts.
+  rewrite top_to_bottom_2.
+  repeat rewrite compose_assoc.
+  rewrite (stack_assoc — —).
+  zx_simpl.
+  repeat rewrite ComposeRules.compose_assoc.
+  rewrite <- (stack_wire_distribute_l ⨉ (— ↕ zx1)).
+  rewrite <- swap_comm.
+  rewrite stack_wire_distribute_l.
+  rewrite <- (ComposeRules.compose_assoc (⨉ ↕ —)).
+  rewrite (stack_assoc_back — (zx1)).
+  zx_simpl.
+  rewrite <- (stack_wire_distribute_r ⨉ (— ↕ zx1)).
+  rewrite <- swap_comm.
+  solve_prop 1.
+  Unshelve.
+  all: lia.
+Qed.
+
+Lemma bigyank_cup : forall (zx1 : ZX 1 1),
+  top_to_bottom 3 ⟷ (⊃ ↕ zx1) ∝ — ↕ ⊃ ⟷ zx1.
+Proof.
+  intros.
+  rewrite (stack_empty_r_rev zx1) at 2.
+  simpl_casts.
+  rewrite <- (stack_compose_distr — zx1).
+  cleanup_zx.
+  rewrite top_to_bottom_grow_l.
+  cleanup_zx.
+  rewrite top_to_bottom_2.
+  rewrite ComposeRules.compose_assoc.
+  rewrite <- (nwire_removal_l ⊃).
+  rewrite <- (wire_removal_r zx1).
+  rewrite (stack_compose_distr).
+  zx_simpl.
+  rewrite <- (ComposeRules.compose_assoc (— ↕ ⨉)).
+  rewrite stack_assoc.
+  simpl_casts.
+  rewrite <- stack_wire_distribute_l.
+  rewrite <- swap_comm.
+  rewrite stack_wire_distribute_l.
+  rewrite <- 2 (ComposeRules.compose_assoc (⨉ ↕ —)).
+  rewrite (stack_assoc_back — zx1 —). 
+  simpl_casts.
+  rewrite <- (stack_wire_distribute_r (⨉) (— ↕ zx1)).
+  rewrite <- swap_comm.
+  zx_simpl.
+  rewrite stack_wire_distribute_r.
+  repeat rewrite ComposeRules.compose_assoc.
+  assert ((⨉ ↕ — ⟷ (— ↕ ⨉ ⟷ (⊃ ↕ —))) ∝ (— ↕ ⊃)) as Hrw. { shelve. }
+  rewrite Hrw; clear Hrw.
+  rewrite (stack_assoc zx1).
+  zx_simpl.
+  bundle_wires.
+  rewrite <- (stack_compose_distr zx1 —).
+  zx_simpl.
+  easy.
+Unshelve.
+  all: try lia.
+  solve_prop 1.
+Qed.
\ No newline at end of file
diff --git a/src/CoreRules/CastRules.v b/src/CoreRules/CastRules.v
index 5b9fe62..b3092e4 100644
--- a/src/CoreRules/CastRules.v
+++ b/src/CoreRules/CastRules.v
@@ -146,7 +146,7 @@ Proof.
 Qed.
 
 Lemma cast_compose_distribute :
-  forall n n' m o o' prfn prfo (zx0 : ZX n m) (zx1 : ZX m o),
+  forall {n} n' {m o} o' prfn prfo (zx0 : ZX n m) (zx1 : ZX m o),
   cast n' o' prfn prfo (zx0 ⟷ zx1) ∝
   cast n' m prfn eq_refl zx0 ⟷ cast m o' eq_refl prfo zx1.
 Proof.
@@ -156,6 +156,18 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma cast_compose_distribute_general :
+  forall {n} n' {m} m' {o} o' prfn prfm prfo (zx0 : ZX n m) (zx1 : ZX m o),
+  cast n' o' prfn prfo (zx0 ⟷ zx1) ∝
+  cast n' m' prfn prfm zx0 ⟷ cast m' o' prfm prfo zx1.
+Proof.
+  intros.
+  subst.
+  simpl_casts.
+  reflexivity.
+Qed.
+
+
 Lemma cast_compose_l :
   forall {n n' m m' o} prfn prfm (zx0 : ZX n m) (zx1 : ZX m' o),
     cast n' m' prfn prfm zx0 ⟷ zx1 ∝ 
diff --git a/src/CoreRules/ComposeRules.v b/src/CoreRules/ComposeRules.v
index b2bbdfb..e4e7ee0 100644
--- a/src/CoreRules/ComposeRules.v
+++ b/src/CoreRules/ComposeRules.v
@@ -110,4 +110,4 @@ Proof.
   rewrite n_wire_semantics.
   Msimpl.
   reflexivity.
-Qed.
+Qed.
\ No newline at end of file
diff --git a/src/CoreRules/CoreAutomation.v b/src/CoreRules/CoreAutomation.v
index f9483c9..39904cb 100644
--- a/src/CoreRules/CoreAutomation.v
+++ b/src/CoreRules/CoreAutomation.v
@@ -39,6 +39,8 @@ Tactic Notation "bundle_wires" := wire_to_n_wire_safe; (* change wires to n_wire
   (fun n m o p => @nwire_stack_compose_topleft n m o p)
   (fun n m o p => @nwire_stack_compose_botleft n m o p)
   : cleanup_zx_db.
+#[export] Hint Rewrite <- nstack1_compose : cleanup_zx_db.
+#[export] Hint Rewrite <- nstack_compose : cleanup_zx_db.
 Tactic Notation "cleanup_zx" := auto_cast_eqn (autorewrite with cleanup_zx_db).
 
 #[export] Hint Rewrite
@@ -62,3 +64,5 @@ Tactic Notation "cleanup_zx" := auto_cast_eqn (autorewrite with cleanup_zx_db).
 Ltac transpose_of H := intros; apply transpose_diagrams; repeat (simpl; autorewrite with transpose_db); apply H.
 Ltac adjoint_of H := intros; apply adjoint_diagrams; repeat (simpl; autorewrite with adjoint_db); apply H.
 Ltac colorswap_of H := intros; apply colorswap_diagrams; repeat (simpl; autorewrite with colorswap_db); apply H.
+
+Ltac zx_simpl := simpl; repeat (cleanup_zx; simpl_casts). 
\ No newline at end of file
diff --git a/src/CoreRules/StackComposeRules.v b/src/CoreRules/StackComposeRules.v
index d1bbb4c..e0df540 100644
--- a/src/CoreRules/StackComposeRules.v
+++ b/src/CoreRules/StackComposeRules.v
@@ -114,4 +114,41 @@ Proof.
   rewrite cast_compose_r.
   simpl_casts.
   easy.
+Qed.
+
+Lemma nstack1_compose : forall n (zx0 zx1 : ZX 1 1),
+	n ↑ zx0 ⟷ n ↑ zx1 ∝ n ↑ (zx0 ⟷ zx1).
+Proof.
+	intros.
+	induction n.
+	- simpl. solve_prop 1.
+	- simpl. rewrite <- (stack_compose_distr zx0 zx1).
+  rewrite IHn.
+  easy.
+Qed.
+	
+
+Lemma colorswap_h_commute_l : forall n m (zx : ZX n m),
+  (n ↑ □) ⟷ zx ∝  (⊙ zx ⟷ (m ↑ □)).
+Proof.
+  intros.
+  rewrite colorswap_is_bihadamard.
+  rewrite 2 compose_assoc.
+  rewrite nstack1_compose.
+  rewrite box_compose.
+  rewrite nwire_removal_r.
+  easy.
+Qed.
+
+Lemma colorswap_h_commute_r : forall {n m} (zx : ZX n m),
+  zx ⟷ (m ↑ □) ∝ ((n ↑ □) ⟷ ⊙ zx).
+Proof.
+  intros.
+  apply colorswap_diagrams.
+  simpl.
+  rewrite 2 n_stack1_colorswap.
+  rewrite colorswap_involutive.
+  simpl.
+  rewrite colorswap_h_commute_l.
+  easy.
 Qed.
\ No newline at end of file
diff --git a/src/CoreRules/StackRules.v b/src/CoreRules/StackRules.v
index 8cc8e57..34c6116 100644
--- a/src/CoreRules/StackRules.v
+++ b/src/CoreRules/StackRules.v
@@ -1,6 +1,7 @@
 Require Export CoreData.CoreData.
 Require Import CastRules.
 Require Import SpiderInduction.
+Require Import ComposeRules.
 
 Local Open Scope ZX_scope.
 
@@ -197,7 +198,7 @@ Unshelve.
 all: lia.
 Qed.
 
-(* Lemma n_wire_collapse_r : forall {n0 n1 m1} (zx0 : ZX n0 0) (zx1 : ZX n1 m1),
+(* Lemma n_wre_collapse_r : forall {n0 n1 m1} (zx0 : ZX n0 0) (zx1 : ZX n1 m1),
  (zx0 ↕ n_wire n1) ⟷ zx1 ∝ zx0 ↕ zx1. *)
 
 Lemma nstack1_split : forall n m (zx : ZX 1 1),
@@ -247,4 +248,47 @@ all: lia.
 Qed.
 
 Lemma nstack1_0 : forall zx, 0 ↑ zx ∝ ⦰.
-Proof. easy. Qed.
\ No newline at end of file
+Proof. easy. Qed.
+
+Lemma nstack_is_nstack1 : forall (zx : ZX 1 1) n prfn prfm, n ⇑ zx ∝ cast _ _ prfn prfm (n ↑ zx).
+Proof.
+	intros.
+	simpl_casts.
+	induction n.
+	- easy.
+	- simpl.
+		rewrite IHn; [ | lia | lia].
+		easy.
+Qed.
+
+Lemma nstack1_is_nstack : forall (zx : ZX 1 1) n prfn prfm, (n ↑ zx) ∝  cast _ _ prfn prfm (n ⇑ zx).
+Proof.
+	intros.
+	rewrite <- cast_symm.
+	rewrite nstack_is_nstack1.
+	easy.
+Unshelve.
+	all: lia.
+Qed.
+
+Lemma nstack_compose : forall n m o n' (zx0 : ZX n m) (zx1 : ZX m o), n' ⇑ (zx0 ⟷ zx1) ∝ n' ⇑ zx0 ⟷ n' ⇑ zx1.
+Proof.
+	intros.
+	induction n'.
+	- simpl. rewrite compose_empty_r. easy.
+	- simpl.
+		rewrite IHn'.
+		rewrite stack_compose_distr.
+    easy.
+Qed.
+
+Lemma nstack1_compose : forall n' (zx0 zx1 : ZX 1 1), n' ↑ (zx0 ⟷ zx1) ∝ n' ↑ zx0 ⟷ n' ↑ zx1.
+Proof.
+	intros.
+  rewrite 3 nstack1_is_nstack.
+	rewrite nstack_compose.
+	rewrite (cast_compose_distribute_general _ n').
+	easy.
+Unshelve.
+all: lia.
+Qed.
diff --git a/src/CoreRules/SwapRules.v b/src/CoreRules/SwapRules.v
index ffb85fe..7595527 100644
--- a/src/CoreRules/SwapRules.v
+++ b/src/CoreRules/SwapRules.v
@@ -133,12 +133,12 @@ Qed.
 Lemma offset_swaps_comm_top_left : 
   ⨉ ↕ — ⟷ (— ↕ ⨉) ∝ 
   — ↕ ⨉ ⟷ (⨉ ↕ —) ⟷ (— ↕ ⨉) ⟷ (⨉ ↕ —).
-Proof. (* solve_prop 1. Qed. *) Admitted.
+Proof. solve_prop 1. Qed. 
 
 Lemma offset_swaps_comm_bot_right : 
  — ↕ ⨉ ⟷ (⨉ ↕ —)  ∝ 
  ⨉ ↕ — ⟷ (— ↕ ⨉) ⟷ (⨉ ↕ —) ⟷ (— ↕ ⨉). 
-Proof. (* solve_prop 1. Qed. *) Admitted.
+Proof. solve_prop 1. Qed.
 
 Lemma bottom_wire_to_top_ind : forall n, bottom_wire_to_top (S (S n)) = @Mmult _ (2 ^ (S (S n))) _ (swap ⊗ (I (2 ^ n))) ((I 2) ⊗ bottom_wire_to_top (S n)).
 Proof.
@@ -284,8 +284,8 @@ Qed.
 Lemma a_swap_3_order_indep :
   I 2 ⊗ swap × (swap ⊗ I 2) × (I 2 ⊗ swap) = (swap ⊗ I 2) × (I 2 ⊗ swap) × (swap ⊗ I 2).
 Proof.
-  (* solve_matrix *) (* Commented out for performance*)
-Admitted.
+  solve_matrix.
+Qed.
 
 Lemma a_swap_semantics_ind : forall n, a_swap_semantics (S (S (S n))) = swap ⊗ (I (2 ^ (S n))) × (I 2 ⊗ a_swap_semantics (S (S n))) × (swap ⊗ (I (2 ^ (S n)))).
 Proof.
@@ -513,38 +513,40 @@ Qed.
 Lemma swap_pullthrough_top_right_Z_1_1 : forall α, (Z 1 1 α) ↕ — ⟷ ⨉ ∝ ⨉ ⟷ (— ↕ (Z 1 1 α)).
 Proof. intros. solve_prop 1. Qed.
 
+Lemma top_to_bottom_2 : top_to_bottom 2 ∝ ⨉.
+Proof.
+  zx_simpl.
+  bundle_wires.
+  zx_simpl.
+  easy.
+Qed.
+
+Opaque top_to_bottom.
 
-Lemma swap_pullthrough_top_right_Z : forall n α prfn prfm, ((Z (S n) 1 α) ↕ —) ⟷ ⨉ ∝ cast _ _ prfn prfm (n_swap _ ⟷ (— ↕ (Z (S n) 1 α))).
+Lemma swap_comm : forall (zx0 zx1 : ZX 1 1),
+  zx0 ↕ zx1 ⟷ ⨉ ∝ ⨉ ⟷ (zx1 ↕ zx0).
 Proof.
-  intro n.
-  induction n; intros.
-  - simpl_casts.
-    cleanup_zx.
-    rewrite n_swap_2_is_swap.
-    rewrite swap_pullthrough_top_right_Z_1_1.
-    easy.
-  - rewrite SpiderInduction.grow_Z_left_2_1 at 1.
-    rewrite stack_wire_distribute_r.
-    rewrite compose_assoc.
-    rewrite IHn.
-    simpl_casts.
-    rewrite n_swap_grow_l.
-    rewrite compose_assoc.
-    rewrite (cast_compose_mid_contract _ (S (S n))).
-    simpl_casts.
-    rewrite (stack_assoc (Z 2 1 _) (n_wire n) —).
-    bundle_wires.
-    rewrite bottom_to_top_grow_r.
-    simpl_casts.
-    rewrite (cast_compose_mid (S (S n))).
-    erewrite <- (@cast_n_wire (S n)).
-    rewrite cast_stack_r.
-    rewrite cast_contract.
-    simpl_casts.
-    erewrite (cast_compose_mid_contract _ (S (S n)) _ _ _ _ _ _ _ (— ↕ bottom_to_top (S n)) (⨉ ↕ n_wire n)).
-    simpl_casts.
-Abort.
+  intros.
+  prop_exists_nonzero 1.
+  Msimpl.
+  simpl.
+  specialize (WF_ZX 1 1 zx0);
+  specialize (WF_ZX 1 1 zx1); intros.
+  solve_matrix.
+Qed.
 
+Transparent top_to_bottom.
+Lemma top_to_bottom_1 : top_to_bottom 1 ∝ —.
+Proof. easy. Qed.
+Opaque top_to_bottom.
+
+Lemma cast_top_to_bottom : forall {n} n' prfn prfn', top_to_bottom n ∝ cast _ _ prfn prfn' (top_to_bottom n').
+Proof.
+  intros.
+  subst.
+  simpl_casts.
+  easy.
+Qed.
 
 Lemma swap_pullthrough_top_right_X_1_1 : forall α, (X 1 1 α) ↕ — ⟷ ⨉ ∝ ⨉ ⟷ (— ↕ (X 1 1 α)).
 Proof. intros. colorswap_of swap_pullthrough_top_right_Z_1_1. Qed.
diff --git a/src/CoreRules/WireRules.v b/src/CoreRules/WireRules.v
index 1ae874b..e01eb21 100644
--- a/src/CoreRules/WireRules.v
+++ b/src/CoreRules/WireRules.v
@@ -1,5 +1,6 @@
 Require Import CoreData.CoreData.
 Require Import StackRules.
+Require Import ComposeRules.
 Require Import CastRules.
 
 Local Open Scope ZX_scope.
@@ -53,9 +54,38 @@ Qed.
 Lemma yank_l : 
   (— ↕ ⊂) ⟷ (⊃ ↕ —) ∝ —.
 Proof.
-  prop_exists_nonzero 1.
+  apply transpose_diagrams.
   simpl.
-  solve_matrix.
+  apply yank_r.
+Qed.
+
+Lemma yank_l_general : forall {n m prfn prfm} (zx0 : ZX n 1) (zx1 : ZX 1 m), 
+  (zx0 ↕ ⊂) ⟷ (⊃ ↕ zx1) ∝ cast _ _ prfn prfm zx0 ⟷ zx1.
+Proof.
+  intros.
+  rewrite <- (wire_removal_l zx1).
+  rewrite <- (wire_removal_r zx0).
+  rewrite <- (nwire_removal_r ⊃).
+  rewrite <- (nwire_removal_l ⊂).
+  simpl.
+  rewrite 2 stack_compose_distr.
+  rewrite compose_assoc.
+  rewrite <- (compose_assoc (— ↕ ⊂)).
+  rewrite yank_l.
+  rewrite stack_empty_r, stack_empty_l.
+  rewrite 2 wire_removal_l, wire_removal_r.
+  easy.
+Qed.
+
+Lemma yank_r_general : forall {n m prfn prfm} (zx0 : ZX n 1) (zx1 : ZX 1 m), 
+(⊂ ↕ zx0) ⟷ (zx1 ↕ ⊃) ∝ zx0 ⟷ cast _ _ prfn prfm zx1.
+Proof.
+  intros.
+  apply transpose_diagrams.
+  simpl.
+  rewrite (@yank_l_general _ _ prfm prfn (zx1)⊤ zx0⊤).
+  rewrite cast_transpose.
+  easy.
 Qed.
 
 Lemma n_wire_stack : forall n m, n_wire n ↕ n_wire m ∝ n_wire (n + m).
diff --git a/src/CoreRules/XRules.v b/src/CoreRules/XRules.v
index 7a7749d..68bf272 100644
--- a/src/CoreRules/XRules.v
+++ b/src/CoreRules/XRules.v
@@ -198,5 +198,17 @@ Proof. transpose_of X_n_wrap_under_r_base. Qed.
 
 (* @nocheck name *)
 (* PI is captialized in Coq R *)
-Lemma X_2_PI : forall n m a, X n m (INR a * 2 * PI) ∝ X n m 0.
-Proof. colorswap_of Z_2_PI. Qed.
+Lemma X_2_PI : forall {n m} a, X n m (IZR a * 2 * PI) ∝ X n m 0.
+Proof. intros. colorswap_of (@Z_2_PI n m a). Qed.
+
+Lemma X_simplify : forall α β n m, α = β -> X n m α ∝ X n m β.
+Proof. intros. subst. easy. Qed.
+
+Lemma X_simplify_general : forall {α β n m} c, α = ((IZR c) * 2 * PI + β)%R -> X n m α ∝ X n m β.
+Proof. intros. colorswap_of (@Z_simplify_general α β n m c). easy. Qed.
+	
+Lemma X_n_swap_absorbtion_left_base : forall n m α, n_swap n ⟷ X n m α ∝ X n m α.
+Proof.
+	colorswap_of Z_n_swap_absorbtion_left_base.
+Qed.
+		
\ No newline at end of file
diff --git a/src/CoreRules/ZRules.v b/src/CoreRules/ZRules.v
index 6f6cae1..22f8672 100644
--- a/src/CoreRules/ZRules.v
+++ b/src/CoreRules/ZRules.v
@@ -6,6 +6,7 @@ Require Import StackComposeRules.
 Require Import SwapRules.
 Require Import WireRules.
 Require Import SpiderInduction.
+Require Import ZArith.
 
 Lemma grow_Z_top_left : forall (nIn nOut : nat) α,
 	Z (S (S nIn)) nOut α ∝  
@@ -35,25 +36,6 @@ Proof.
 	apply grow_Z_top_left.
 Qed.
 
-Lemma grow_Z_bot_left : forall n {m o α},
-	Z (n + m) o α ∝ 
-	(n_wire n ↕ Z m 1 0) ⟷ Z (n + 1) o α.
-Proof.
-Admitted.
-
-Lemma grow_Z_bot_right : forall {n m} o {α},
-	Z n (m + o) α ∝ 
-	Z n (m + 1) α ⟷ (n_wire m ↕ Z 1 o 0).
-Proof.
-	intros.
-	apply transpose_diagrams.
-	simpl.
-	rewrite nstack1_transpose.
-	rewrite transpose_wire.
-	apply grow_Z_bot_left.
-Qed.
-
-
 Lemma Z_rot_l : forall n m α β,
 	Z (S n) m (α + β) ∝ Z 1 1 α ↕ n_wire n ⟷ Z (S n) m β.
 Proof.
@@ -688,6 +670,12 @@ Unshelve.
   all: lia.
 Qed.
 
+Lemma Z_n_swap_absorbtion_left_base : forall n m α, n_swap n ⟷ Z n m α ∝ Z n m α.
+Proof.
+	transpose_of Z_n_swap_absorbtion_right_base.
+Qed.
+
+
 Lemma Z_n_wrap_under_r_base_unswapped : forall n m α, Z (n + m) 0 α ∝ (Z n m α ↕ n_wire m) ⟷ n_cup_unswapped m.
 Proof.
 	intros.
@@ -829,11 +817,21 @@ Qed.
 Lemma Z_n_wrap_over_r_base : forall n m α, Z (m + n) 0 α ∝ (n_wire m ↕ Z n m α) ⟷ n_cup m.
 Proof.
 	intros.
-	rewrite n_cup_inv_n_swap_n_wire.
+	unfold n_cup.
 	rewrite <- compose_assoc.
-	rewrite <- stack_nwire_distribute_l.
-	rewrite Z_n_swap_absorbtion_right_base.
-	rewrite Z_n_wrap_over_r_base_unswapped.
+	rewrite <- stack_compose_distr.
+	cleanup_zx.
+	rewrite <- (nwire_removal_l (Z n m α)).
+	rewrite <- (nwire_removal_r (n_swap m)).
+	rewrite stack_compose_distr.
+	rewrite compose_assoc.
+	rewrite <- Z_n_wrap_over_r_base_unswapped.
+	rewrite Z_add_l_base_rot.
+	rewrite <- compose_assoc.
+	rewrite <- stack_compose_distr.
+	cleanup_zx.
+	rewrite Z_n_swap_absorbtion_left_base.
+	rewrite <- Z_add_l_base_rot.
 	easy.
 Qed.
 
@@ -851,14 +849,67 @@ Proof. transpose_of Z_n_wrap_under_r_base. Qed.
 
 (* @nocheck name *)
 (* PI is captialized in Coq R *)
-Lemma Z_2_PI : forall n m a, Z n m (INR a * 2 * PI) ∝ Z n m 0.
+Lemma Z_2_PI : forall {n m} a, Z n m (IZR a * 2 * PI) ∝ Z n m 0.
 Proof.
 	intros.
 	prop_exists_nonzero 1.
 	Msimpl.
 	simpl.
-	unfold Z_semantics. 
-	rewrite Cexp_2_PI.
-	rewrite Cexp_0.
+	unfold Z_semantics.
+	replace ((IZR a * 2))%R with (IZR (a * 2))%R by (rewrite mult_IZR; simpl; lra).
+	rewrite Cexp_mod_2PI.
+	rewrite Z_mod_mult.
+	rewrite Rmult_0_l.
+	autorewrite with Cexp_db.
 	easy.
 Qed.
+
+Lemma grow_Z_bot_left : forall n {m o α},
+	Z (n + m) o α ∝ 
+	(n_wire n ↕ Z m 1 0) ⟷ Z (n + 1) o α.
+Proof.
+	induction n; intros.
+	- simpl.
+		cleanup_zx.
+		rewrite Z_absolute_fusion.
+		rewrite Rplus_0_l.
+		easy.
+	- simpl. 
+		rewrite  (Z_wrap_over_top_left ((n + 1))).
+		rewrite <- compose_assoc.
+		rewrite (stack_assoc — (n ↑ —)).
+		simpl_casts.
+		rewrite <- (stack_compose_distr — —).
+		rewrite <- IHn.
+		cleanup_zx.
+		rewrite <- Z_wrap_over_top_left.
+		easy.
+	Unshelve.
+	all: lia.
+Qed.
+
+Lemma grow_Z_bot_right : forall {n m} o {α},
+	Z n (m + o) α ∝ 
+	Z n (m + 1) α ⟷ (n_wire m ↕ Z 1 o 0).
+Proof.
+	intros.
+	apply transpose_diagrams.
+	simpl.
+	rewrite nstack1_transpose.
+	rewrite transpose_wire.
+	apply grow_Z_bot_left.
+Qed.
+
+
+Lemma Z_simplify : forall α β n m, α = β -> Z n m α ∝ Z n m β.
+Proof. intros. subst. easy. Qed.
+	
+Lemma Z_simplify_general : forall {α β n m} c, α = ((IZR c) * 2 * PI + β)%R -> Z n m α ∝ Z n m β.
+Proof. 
+	intros; subst. 
+	rewrite <- Z_spider_1_1_fusion. 
+	rewrite (Z_2_PI c).
+	rewrite Z_spider_1_1_fusion.
+	apply Z_simplify.
+	lra.
+Qed.
\ No newline at end of file
diff --git a/src/CoreRules/ZXRules.v b/src/CoreRules/ZXRules.v
index f1afa10..81fe1e8 100644
--- a/src/CoreRules/ZXRules.v
+++ b/src/CoreRules/ZXRules.v
@@ -191,6 +191,52 @@ Proof.
 	all: lia.
 Qed.
 
+Lemma Z_X_pi_comm : forall α,
+	Z 1 1 PI ⟷ X 1 1 α ∝
+	X 1 1 (-α) ⟷ Z 1 1 PI.
+Proof.
+	intros.
+	prop_exists_nonzero (Cexp α).
+	repeat rewrite ZX_semantic_equiv.
+	Msimpl.
+	simpl.
+	Msimpl.
+	repeat rewrite Mmult_plus_distr_l.
+	repeat rewrite Mmult_plus_distr_r.
+	autorewrite with scalar_move_db.
+	repeat rewrite Mmult_assoc.
+	restore_dims.
+	repeat rewrite <- (Mmult_assoc ⟨-∣).
+	repeat rewrite <- (Mmult_assoc ⟨+∣).
+	repeat rewrite <- (Mmult_assoc ⟨1∣).
+	repeat rewrite <- (Mmult_assoc ⟨0∣).
+	autorewrite with ketbra_mult_db.
+	autorewrite with scalar_move_db.
+	Msimpl.
+	rewrite Cexp_PI.
+	replace (-1 * - / (√ 2)%R) with (/ (√2)%R) by lca.
+	rewrite Mscale_plus_distr_r.
+	repeat rewrite Mscale_assoc.
+	replace (-1 * (Cexp α * - / (√ 2)%R)) with (Cexp α * / (√2)%R) by lca.
+	replace (-1 * / (√ 2)%R) with (-/(√2)%R) by lca.
+	repeat rewrite Mscale_plus_distr_r.
+	repeat rewrite Mscale_assoc.
+	replace (Cexp α * Cexp (-α)) with C1.
+	rewrite Cmult_1_l.
+	lma.
+	rewrite <- Cexp_add.
+	rewrite Rplus_opp_r.
+	rewrite Cexp_0.
+	easy.
+Qed.
+
+Lemma X_Z_pi_comm : forall α,
+	X 1 1 PI ⟷ Z 1 1 α ∝
+	Z 1 1 (-α) ⟷ X 1 1 PI.
+Proof.
+	colorswap_of Z_X_pi_comm.
+Qed.
+
 Lemma X_copy : forall n r prfn prfm,
 	(X 1 1 (INR r * PI) ⟷ Z 1 n 0) ∝
 	Z 1 n 0 ⟷ 
@@ -207,58 +253,143 @@ Proof.
 	apply Z_copy.
 Qed.
 
-Lemma Z_0_copy : forall n prfn prfm, 
-	(Z 1 1 0 ⟷ X 1 n 0) ∝
-	X 1 n 0 ⟷ 
-		(cast n n prfn prfm
-			(n ⇑ (Z 1 1 0))).
+
+
+Lemma Z_0_copy_base : forall α, Z 1 1 0 ⟷ X 1 0 α ∝ X 1 0 (α).
 Proof.
 	intros.
-	specialize (Z_copy n 0).
+	simpl.
+	prop_exists_nonzero 1.
+	simpl.
+	unfold X_semantics, Z_semantics.
+	simpl.
+	solve_matrix.
+	autorewrite with Cexp_db.
+	lca.
+Qed.
+
+Lemma X_0_copy_base : forall α, X 1 1 0 ⟷ Z 1 0 α ∝ Z 1 0 (α).
+Proof.
 	intros.
-	simpl in H.
-	rewrite Rmult_0_l in H.
-	apply H.
+	colorswap_of Z_0_copy_base.
 Qed.
 
-Lemma Z_pi_copy : forall n prfn prfm, 
-	(Z 1 1 PI ⟷ X 1 n 0) ∝
-	X 1 n 0 ⟷ 
-		(cast n n prfn prfm
-			(n ⇑ (Z 1 1 PI))).
+
+Lemma Z_pi_copy_base : forall α, Z 1 1 (INR 1 * PI) ⟷ X 1 0 α ∝ X 1 0 (-α).
+Proof.
+	intros.
+	simpl.
+	prop_exists_nonzero (Cexp α).
+	simpl.
+	rewrite Rmult_1_l.
+	unfold X_semantics, Z_semantics.
+	simpl.
+	solve_matrix.
+	autorewrite with Cexp_db.
+	rewrite Cmult_plus_distr_l.
+	rewrite Cmult_assoc.
+	rewrite Cinv_r.
+	lca.
+	nonzero.
+	field_simplify.
+	autorewrite with Cexp_db.
+	repeat rewrite <- Copp_mult_distr_l.
+	field_simplify.
+	lca.
+	all:nonzero.
+Qed.
+
+Lemma X_pi_copy_base : forall α, X 1 1 (INR 1 * PI) ⟷ Z 1 0 α ∝ Z 1 0 (-α).
 Proof.
 	intros.
-	specialize (Z_copy n 1).
+	colorswap_of Z_pi_copy_base.
+Qed.
+
+Lemma Z_0_copy : forall n α, 
+	(Z 1 1 0 ⟷ X 1 n α) ∝
+	X 1 n α.
+Proof.
 	intros.
-	simpl in H.
-	rewrite Rmult_1_l in H.
-	apply H.
+	replace (α) with (α + 0+ 0)%R by lra.
+	rewrite (@X_add_r 1%nat 0%nat n) at 1.
+	rewrite <- compose_assoc.
+	replace 0%R with (INR 0 * PI)%R at 01 by (simpl; lra).
+	rewrite Z_copy at 1.
+	simpl_casts.
+	simpl.
+	cleanup_zx.
+	simpl_casts.
+	rewrite compose_assoc.
+	rewrite <- (stack_compose_distr (Z 1 1 (0 * PI)) (X 1 0 α) (Z 1 1 (0 * PI)) (X 1 n 0)).
+	replace (0 * PI)%R with (INR 0 * PI)%R by easy.
+	rewrite Z_copy.
+	simpl.
+	rewrite Rmult_0_l.
+	rewrite Z_0_copy_base.
+	rewrite <- (nwire_removal_r (X 1 0 _)).
+	rewrite stack_compose_distr.
+	rewrite <- compose_assoc.
+	rewrite <- X_add_r.
+	simpl_casts.
+	simpl.
+	cleanup_zx.
+	rewrite nstack_is_nstack1.
+	simpl_casts.
+	cleanup_zx.
+	easy.
+Unshelve.
+all: lia.
 Qed.
 
-Lemma X_0_copy : forall n prfn prfm, 
-	(X 1 1 0 ⟷ Z 1 n 0) ∝
-	Z 1 n 0 ⟷ 
+Lemma Z_pi_copy : forall n α prfn prfm, 
+	(Z 1 1 PI ⟷ X 1 n α) ∝
+	X 1 n (-α) ⟷ 
 		(cast n n prfn prfm
-			(n ⇑ (X 1 1 0))).
+			(n ⇑ (Z 1 1 PI))).
 Proof.
 	intros.
-	specialize (X_copy n 0).
+	replace (α) with (α + 0+ 0)%R by lra.
+	rewrite (@X_add_r 1%nat 0%nat n).
+	rewrite <- compose_assoc.	
+	replace (PI) with (INR 1 * PI)%R by (simpl; lra).
+	rewrite Z_copy.
+	simpl_casts.
+	simpl.
+	cleanup_zx.
+	simpl_casts.
+	rewrite compose_assoc.
+	rewrite <- (stack_compose_distr (Z 1 1 (1 * PI)) (X 1 0 α) (Z 1 1 (1 * PI)) (X 1 n 0)).
+	replace (1 * PI)%R with (INR 1 * PI)%R by easy.
+	rewrite Z_copy.
+	rewrite Z_pi_copy_base.
+	rewrite <- (nwire_removal_r (X 1 0 _)).
+	rewrite stack_compose_distr.
+	rewrite <- compose_assoc.
+	rewrite <- X_add_r.
+	apply compose_simplify.
+	apply X_simplify; lra.
+	simpl.
+	cleanup_zx.
+	easy.
+Unshelve.
+all: lia.
+Qed.
+
+
+Lemma X_0_copy : forall n α, 
+	(X 1 1 0 ⟷ Z 1 n α) ∝
+	Z 1 n α.
+Proof.
 	intros.
-	simpl in H.
-	rewrite Rmult_0_l in H.
-	apply H.
+	colorswap_of Z_0_copy.
 Qed.
 
-Lemma X_pi_copy : forall n prfn prfm, 
-	(X 1 1 PI ⟷ Z 1 n 0) ∝
-	Z 1 n 0 ⟷ 
+Lemma X_pi_copy : forall n α prfn prfm, 
+	(X 1 1 PI ⟷ Z 1 n α) ∝
+	Z 1 n (-α) ⟷ 
 		(cast n n prfn prfm
 			(n ⇑ (X 1 1 PI))).
 Proof.
 	intros.
-	specialize (X_copy n 1).
-	intros.
-	simpl in H.
-	rewrite Rmult_1_l in H.
-	apply H.
+	colorswap_of Z_pi_copy.
 Qed.
\ No newline at end of file
diff --git a/src/DiagramRules/Bell.v b/src/DiagramRules/Bell.v
index f65d316..1be216c 100644
--- a/src/DiagramRules/Bell.v
+++ b/src/DiagramRules/Bell.v
@@ -84,6 +84,7 @@ Proof.
   rewrite <- (stack_compose_distr (X 0 (1 + 1) _) (n_wire 1 ↕ X 1 1 _) (Z 1 (1 + 0) _) (X 1 1 _)).
   rewrite (dominated_X_spider_fusion_bot_left 1 0).
   replace ((INR b * PI + (INR b * PI + 0)))%R with (INR b * 2 * PI)%R by lra.
+  rewrite (INR_IZR_INZ b).
   rewrite X_2_PI.
   rewrite X_0_is_wire.
   rewrite <- (nwire_removal_l (X 0 _ _)).
@@ -96,6 +97,7 @@ Proof.
   cleanup_zx; simpl_casts.
   rewrite Z_spider_1_1_fusion.
   replace (INR a * PI + 0 + INR a * PI)%R with ((INR a * 2 * PI))%R by lra.
+  rewrite (INR_IZR_INZ a).
   rewrite Z_2_PI.
   rewrite Z_0_is_wire.
   easy.
diff --git a/src/DiagramRules/Bialgebra.v b/src/DiagramRules/Bialgebra.v
index f282b22..5094df3 100644
--- a/src/DiagramRules/Bialgebra.v
+++ b/src/DiagramRules/Bialgebra.v
@@ -1,73 +1,40 @@
 Require Import CoreData.
 Require Import CoreRules.
 
-Definition bi_alg_Z_X := ((Z_Spider 1 2 0) ↕ (Z_Spider 1 2 0) ⟷ (— ↕ ⨉ ↕ —) ⟷ ((X_Spider 2 1 0) ↕ (X_Spider 2 1 0))).
-Definition bi_alg_X_Z := ((X_Spider 1 2 0) ↕ (X_Spider 1 2 0) ⟷ (— ↕ ⨉ ↕ —) ⟷ ((Z_Spider 2 1 0) ↕ (Z_Spider 2 1 0))).
+Definition bi_alg_Z_X := ((Z 1 2 0) ↕ (Z 1 2 0) ⟷ (— ↕ ⨉ ↕ —) ⟷ ((X 2 1 0) ↕ (X 2 1 0))).
+Definition bi_alg_X_Z := ((X 1 2 0) ↕ (X 1 2 0) ⟷ (— ↕ ⨉ ↕ —) ⟷ ((Z 2 1 0) ↕ (Z 2 1 0))).
 
 Theorem bi_algebra_rule_Z_X : 
- (X_Spider 2 1 0) ⟷ (Z_Spider 1 2 0) ∝ bi_alg_Z_X.
+ X 2 1 0 ⟷ Z 1 2 0 ∝ bi_alg_Z_X.
 Proof.
-  prop_exists_nonzero 1.
-  simpl.
-  rewrite X_semantics_equiv, Z_semantics_equiv.
+  prop_exists_nonzero (√ 2)%R.
+  rewrite 2 ZX_semantic_equiv.
   unfold_dirac_spider.
   autorewrite with Cexp_db.
-  Msimpl.
-  repeat rewrite kron_plus_distr_l.
-  repeat rewrite kron_plus_distr_r.
-  repeat rewrite kron_plus_distr_l.
-  repeat rewrite Mmult_plus_distr_l.
-  repeat rewrite Mmult_plus_distr_r.
-  repeat rewrite Mmult_plus_distr_l.
-  assert (forall (ket0 : Matrix 2 1) (bra0 : Matrix 1 2) (ket1 : Matrix 2 1) (bra1 : Matrix 1 2), 
-  WF_Matrix ket0 -> WF_Matrix ket1 ->
-  ket0⊤ = bra0 -> ket1⊤ = bra1 ->
-  (ket0 × (bra0 ⊗ bra0)) ⊗ (ket1 × (bra1 ⊗ bra1)) × (I 2 ⊗ swap ⊗ I 2) 
-  = (ket0 × (bra0 ⊗ bra1) ⊗ (ket1 × (bra0 ⊗ bra1))))%M.
-  {
-    intros.
-    subst bra0 bra1.
-    rewrite kron_assoc; try auto with wf_db.
-    rewrite <- 2 kron_mixed_product.
-    rewrite Mmult_assoc.
-    apply Mmult_simplify; [ easy | ].
-    restore_dims.
-    repeat rewrite kron_assoc by auto with wf_db.
-    rewrite (kron_mixed_product (ket0⊤) (ket0⊤ ⊗ (ket1⊤ ⊗ ket1⊤)) (I 2) _)%M.
-    Msimpl.
-    apply kron_simplify; [ easy | ].
-    rewrite <- 2 kron_assoc by auto with wf_db.
-    rewrite (kron_mixed_product (ket0⊤ ⊗ ket1⊤) (ket1⊤) swap _)%M.
-    Msimpl.
-    apply kron_simplify; [ | easy].
-    apply transpose_matrices.
-    rewrite Mmult_transpose.
-    rewrite swap_transpose.
-    rewrite <- 2 kron_transpose.
-    rewrite 2 Matrix.transpose_involutive.
-    rewrite swap_spec by auto with wf_db.
-    easy.
-  }
-  repeat rewrite <- Mmult_assoc.
-  restore_dims.
-  rewrite bra0_equiv, bra1_equiv, ket0_equiv, ket1_equiv.
-  repeat rewrite H; try auto with wf_db.
-  2-9: apply transpose_matrices; try rewrite braplus_transpose_ketplus; try rewrite braminus_transpose_ketminus; rewrite Matrix.transpose_involutive; easy.
-  restore_dims.
-  repeat rewrite (kron_mixed_product (xbasis_plus × (_ ⊗ _)) (xbasis_plus × (_ ⊗ _))  ((ket _ ⊗ ket _) × bra _) ((ket _ ⊗ ket _) × bra _)).
-  repeat rewrite (kron_mixed_product (xbasis_minus × (_ ⊗ _)) (xbasis_minus × (_ ⊗ _))  ((ket _ ⊗ ket _) × bra _) ((ket _ ⊗ ket _) × bra _)).
-  repeat rewrite Mmult_assoc.
-Admitted.
+  simpl.
+  unfold xbasis_plus, xbasis_minus.
+  repeat rewrite kron_1_l; try auto with wf_db.
+  repeat rewrite Mscale_1_l.
+  repeat rewrite Mmult_adjoint.
+  repeat rewrite hadamard_sa.
+  repeat rewrite ket2bra.
+  autorewrite with scalar_move_db.
+  apply Mscale_simplify; [ | C_field_simplify; [easy | nonzero]].
+  solve_matrix.
+  all: unfold braplus, braminus, scale, Mplus, adjoint, qubit0, qubit1.
+  all: repeat rewrite Cconj_R.
+  all: C_field_simplify; [ lca | nonzero].
+Qed.
 
 Theorem bi_algebra_rule_X_Z : 
- (Z_Spider 2 1 0) ⟷ (X_Spider 1 2 0) ∝ bi_alg_X_Z.
+ Z 2 1 0 ⟷ X 1 2 0 ∝ bi_alg_X_Z.
 Proof.
   colorswap_of bi_algebra_rule_Z_X.
 Qed.
 
 
 Theorem hopf_rule_Z_X : 
-  (Z_Spider 1 2 0) ⟷ (X_Spider 2 1 0) ∝ (Z_Spider 1 0 0) ⟷ (X_Spider 0 1 0).
+  Z 1 2 0 ⟷ X 2 1 0 ∝ Z 1 0 0 ⟷ X 0 1 0.
 Proof.
   intros.
   rewrite <- (@nwire_removal_r 2).
@@ -180,7 +147,7 @@ all: lia.
 Qed.
 
 Theorem hopf_rule_X_Z : 
-  (X_Spider 1 2 0) ⟷ (Z_Spider 2 1 0) ∝ (X_Spider 1 0 0) ⟷ (Z_Spider 0 1 0).
+  (X 1 2 0) ⟷ (Z 2 1 0) ∝ (X 1 0 0) ⟷ (Z 0 1 0).
 Proof.
   colorswap_of hopf_rule_Z_X.
 Qed.
\ No newline at end of file
diff --git a/src/Gates/GateRules.v b/src/Gates/GateRules.v
index f15489c..8f4213f 100644
--- a/src/Gates/GateRules.v
+++ b/src/Gates/GateRules.v
@@ -132,10 +132,10 @@ Unshelve.
 all: lia.
 Qed.
 
-Lemma cnot_is_cnot_r : _CNOT_ ∝ _CNOT_R.
+Lemma cnot_is_cnot_r_general : forall α β, Z 1 2 α ↕ — ⟷ (— ↕ X 2 1 β) ∝ — ↕ X 1 2 β ⟷ (Z 2 1 α ↕ —).
 Proof.
   intros.
-  remember (— ↕ X 1 2 0 ⟷ (Z 2 1 0 ↕ —)) as RHS.
+  remember (— ↕ X 1 2 _ ⟷ (Z 2 1 _ ↕ —)) as RHS.
   rewrite (Z_wrap_under_bot_left 1 1).
   rewrite (X_wrap_over_top_left 1 1).
   simpl_casts.
@@ -143,17 +143,17 @@ Proof.
   rewrite stack_nwire_distribute_l.
   rewrite stack_nwire_distribute_r.
   repeat rewrite <- compose_assoc.
-  rewrite (compose_assoc _ (Z (1 + 1) 1 0 ↕ (n_wire _) ↕ _)).
+  rewrite (compose_assoc _ (Z (1 + 1) 1 _ ↕ (n_wire _) ↕ _)).
   rewrite stack_assoc.
   simpl_casts.
   rewrite n_wire_stack.
-  rewrite (nwire_stack_compose_botleft (Z (1 + 1) 1 0) (n_wire 1 ↕ X 1 2 0)).
-  rewrite <- (nwire_stack_compose_topleft (n_wire 1 ↕ X 1 2 0)).
+  rewrite (nwire_stack_compose_botleft (Z (1 + 1) 1 _) (n_wire 1 ↕ X 1 2 _)).
+  rewrite <- (nwire_stack_compose_topleft (n_wire 1 ↕ X 1 2 _)).
   rewrite <- compose_assoc.
   rewrite stack_assoc_back.
   simpl_casts.
   rewrite n_wire_stack.
-  rewrite <- (stack_compose_distr ((n_wire 1) ↕ ⊂) (n_wire 3) (n_wire 1) (X 1 2 0)).
+  rewrite <- (stack_compose_distr ((n_wire 1) ↕ ⊂) (n_wire 3) (n_wire 1) (X 1 2 _)).
   cleanup_zx.
   rewrite <- nwire_stack_compose_topleft.
   rewrite compose_assoc.
@@ -175,14 +175,33 @@ Unshelve.
 all: lia.
 Qed.
 
+Lemma cnot_is_cnot_r : _CNOT_ ∝ _CNOT_R.
+Proof.
+  apply cnot_is_cnot_r_general.
+Qed.
+
 Lemma cnot_inv_is_swapped_cnot : _CNOT_inv_ ∝ ⨉ ⟷ _CNOT_ ⟷ ⨉.
-Admitted.
+Proof.
+  solve_prop 1.
+Qed.
 
 Lemma notc_is_swapp_cnot : _NOTC_ ∝ ⨉ ⟷ _CNOT_ ⟷ ⨉. 
-Admitted.
+Proof.
+  rewrite <- cnot_inv_is_swapped_cnot.
+  rewrite compose_assoc.
+  rewrite <- colorswap_is_bihadamard.
+  rewrite cnot_is_cnot_r.
+  easy.
+Qed.
 
 Lemma notc_r_is_swapp_cnot_r : _NOTC_R ∝ ⨉ ⟷ _CNOT_R ⟷ ⨉. 
-Admitted.
+Proof.
+  rewrite <- cnot_is_cnot_r.
+  rewrite <- cnot_inv_is_swapped_cnot.
+  rewrite compose_assoc.
+  rewrite <- colorswap_is_bihadamard.
+  easy.
+Qed.
 
 Lemma notc_is_notc_r : _NOTC_ ∝ _NOTC_R.
 Proof.
@@ -190,4 +209,13 @@ Proof.
   rewrite cnot_is_cnot_r.
   rewrite <- notc_r_is_swapp_cnot_r.
   easy.
+Qed.
+
+Lemma notc_is_notc_r_general : forall α β, — ↕ Z 1 2 α ⟷ (X 2 1 β ↕ —) ∝ X 1 2 β ↕ — ⟷ (— ↕ Z 2 1 α).
+Proof. 
+  intros.
+  apply colorswap_diagrams.
+  simpl.
+  rewrite cnot_is_cnot_r_general.
+  easy.
 Qed.
\ No newline at end of file
diff --git a/src/Ingest/Interact.v b/src/Ingest/Interact.v
new file mode 100644
index 0000000..e15fc0f
--- /dev/null
+++ b/src/Ingest/Interact.v
@@ -0,0 +1,71 @@
+Require Import SQIR.UnitarySem.
+Require Import SQIR.Equivalences.
+Require Import QuantumLib.Quantum.
+Require Import CoreData.
+Require Import CoreRules.
+Require Import Gates.
+Require Import ZXPad.
+Require Import VOQC.RzQGateSet.
+Require Import VOQC.UnitaryListRepresentation.
+Require Import Ingest.
+
+Local Open Scope ZX_scope.
+
+Definition scalar_equiv_ucom {dim} (l o : ucom RzQGateSet.U dim) := (RzQToBaseUCom l) ≡ (RzQToBaseUCom o) by uc_eval. 
+Notation "l '≡u' o" := (scalar_equiv_ucom l o) (at level 80).
+
+Lemma prop_implies_scalar_equiv_rz_q {dim} : forall (l o : ucom RzQGateSet.U dim),
+  uc_well_typed l -> uc_well_typed o ->
+  ingest l ∝ ingest o -> l ≡u o.
+Proof.
+  unfold scalar_equiv_ucom.
+  unfold proportional_general.
+  intros l o WTl WTo [c [semeq cnz]].
+  unfold uc_equiv.
+  destruct (ingest_correct l); [auto | ].
+  destruct (ingest_correct o); [auto | ].
+  destruct H.
+  destruct H0.
+  rewrite <- H in semeq.
+  rewrite <- H0 in semeq.
+  exists  ((c * x0) / x)%C.
+  split.
+  - unfold Cdiv.
+    rewrite (Cmult_comm (c * x0)).
+    rewrite <- Mscale_assoc.
+    rewrite <- Mscale_assoc.
+    rewrite <- semeq.
+    repeat rewrite Mscale_assoc.
+    replace (/ x * x)%C with (C1).
+    lma.
+    rewrite Cmult_comm.
+    rewrite Cinv_r; auto.
+  - unfold Cdiv.
+    apply Cmult_neq_0; auto.
+    apply Cmult_neq_0; auto.
+    apply nonzero_div_nonzero; auto.
+Qed.
+
+Local Open Scope ucom.
+Local Open Scope matrix_scope.
+Ltac solve_uc_well_typed :=
+  match goal with
+  | [ |- uc_well_typed (useq ?c ?c2) ] => apply WT_seq; solve_uc_well_typed
+  | [ |- uc_well_typed (@SQIR.H ?dim ?n) ] => apply uc_well_typed_H
+  | [ |- uc_well_typed (@SQIR.X ?dim ?n) ] => apply uc_well_typed_X
+  | [ |- uc_well_typed (@SQIR.Y ?dim ?n) ] => apply uc_well_typed_Y
+  | [ |- uc_well_typed (@SQIR.ID ?dim ?n) ] => apply uc_well_typed_ID
+  | [ |- uc_well_typed (@SQIR.Rx ?dim ?θ ?n) ] => apply uc_well_typed_Rx
+  | [ |- uc_well_typed (@SQIR.Ry ?dim ?θ ?n) ] => apply uc_well_typed_Ry
+  | [ |- uc_well_typed (@SQIR.Rz ?dim ?θ ?n) ] => apply uc_well_typed_Rz
+  | [ |- uc_well_typed (@SQIR.CNOT ?dim ?m ?n) ] => apply uc_well_typed_CNOT
+  | [ |- uc_well_typed (@SQIR.SWAP ?dim ?m ?n) ] => apply uc_well_typed_SWAP
+  | [ |- uc_well_typed (uapp1 ?u ?n)] => apply (@WT_app1 u n); try lia
+  | [ |- uc_well_typed (uapp2 ?u ?m ?n)] =>  apply (@WT_app2 u m n); try lia
+  | [ |- uc_well_typed (uapp3 ?u ?m ?n ?p)] =>  apply (@WT_app3 u m n p); try lia
+  end.
+
+Ltac circuit_to_zx := apply prop_implies_scalar_equiv_rz_q; [ solve_uc_well_typed | solve_uc_well_typed | ].
+
+Ltac circuit_to_zx_b := apply prop_implies_scalar_equiv_rz_q; [ apply uc_well_typed_b_equiv; easy | apply uc_well_typed_b_equiv; easy | ].
+
diff --git a/src/Ingest/Peephole.v b/src/Ingest/Peephole.v
new file mode 100644
index 0000000..edf11f2
--- /dev/null
+++ b/src/Ingest/Peephole.v
@@ -0,0 +1,533 @@
+Require Import SQIR.UnitarySem.
+Require Import SQIR.Equivalences.
+Require Import QuantumLib.Quantum.
+Require Import Gates.
+Require Import ZXPad.
+Require Import VOQC.RzQGateSet.
+Require Import VOQC.UnitaryListRepresentation.
+Require Import Ingest.
+Require Import Interact.
+Require Import SQIR.SQIR.
+Require Import VOQC.RzQGateSet.
+
+Require Import CoreRules.
+Require Import CoreData.
+Require Import CoreRules.ComposeRules.
+
+Definition U := RzQ_Unitary.
+
+Local Open Scope ucom_scope.
+
+(* @nocheck name *)
+(* Qualifier *)
+Definition RZCNOT {dim} o p : ucom U dim := uapp2 (URzQ_CNOT) o p.
+(* @nocheck name *)
+(* Qualifier *)
+Definition RZRZ {dim} q t : ucom U dim := uapp1 (URzQ_Rz q) t.
+(* @nocheck name *)
+(* Qualifier *)
+Definition RZH {dim} t : ucom U dim := uapp1 (URzQ_H) t.
+(* Qualifier *)
+(* @nocheck name *)
+Definition RZX {dim} t : ucom U dim := uapp1 (URzQ_X) t.
+(* @nocheck name *)
+(* Qualifier *)
+Definition SKIP {dim} : ucom U dim := uapp1 (URzQ_Rz 0) 0.
+(* @nocheck name *)
+(* Qualifier *)
+Definition RZP {dim} t : ucom U dim := uapp1 (URzQ_Rz (1 / 2)) t.
+(* @nocheck name *)
+(* Qualifier *)
+Definition RZPdag {dim} t : ucom U dim := uapp1 (URzQ_Rz (3 / 2)) t.
+
+Local Open Scope ZX_scope.
+
+Local Hint Unfold ingest : RzQ_to_ZX.
+Local Hint Unfold cnot_ingest : RzQ_to_ZX.
+Local Hint Unfold H_ingest : RzQ_to_ZX.
+Local Hint Unfold Rz_ingest : RzQ_to_ZX.
+Local Hint Unfold gate_ingest : RzQ_to_ZX.
+Local Hint Unfold gate_ingest' : RzQ_to_ZX.
+Local Hint Unfold pad_top : RzQ_to_ZX.
+Local Hint Unfold pad_bot : RzQ_to_ZX.
+Local Hint Unfold pad_bot_1 : RzQ_to_ZX.
+Local Hint Unfold cnot_n_m_ingest : RzQ_to_ZX.
+Local Hint Unfold cnot_m_n_ingest : RzQ_to_ZX.
+Local Hint Unfold unpadded_cnot : RzQ_to_ZX.
+Local Hint Unfold _Rz_ : RzQ_to_ZX.
+Local Hint Unfold base_cnot : RzQ_to_ZX.
+Local Hint Unfold bottom_to_top : RzQ_to_ZX.
+Local Hint Unfold top_to_bottom : RzQ_to_ZX.
+
+Ltac circuit_to_zx_full := circuit_to_zx_b; autounfold with RzQ_to_ZX; simpl;
+  cleanup_zx; simpl_casts.
+
+Lemma cnot_flip : @RZH 2 0 ; RZH 1 ; RZCNOT 0 1; RZH 0; RZH 1 ≡u RZCNOT 1 0.
+Proof.
+  circuit_to_zx_full.
+  rewrite compose_assoc.
+  rewrite <- (stack_compose_distr □ —).
+  cleanup_zx.
+  easy.
+Qed.
+
+(* Hadamard reductions from fig 4 in Nam et al*)
+
+Lemma h_p_reduction : □ ⟷ Z 1 1 ((1 / 2) * PI) ⟷ □
+∝ Z 1 1 ((3 / 2) * PI) ⟷ □ ⟷ Z 1 1 ((3 / 2) * PI).
+Proof.   
+  rewrite compose_assoc.
+  rewrite <- (nstack1_1 □) at 1 2.
+  rewrite <- colorswap_is_bihadamard.
+  simpl.
+  rewrite <- _H_is_box.
+  repeat rewrite compose_assoc.
+  rewrite Z_spider_1_1_fusion.
+  repeat rewrite <- compose_assoc.
+  rewrite Z_spider_1_1_fusion.
+  replace (3 / 2 * PI + PI / 2)%R with ((INR 1) * 2 * PI)%R by (simpl; lra).
+  replace (PI / 2 + 3 / 2 * PI)%R with ((INR 1) * 2 * PI)%R by (simpl; lra).
+  rewrite INR_IZR_INZ.
+  rewrite Z_2_PI.
+  cleanup_zx.
+  apply X_simplify.
+  lra.
+Qed. 
+
+Lemma remove_q_2_r12 : Q2R (1 / 2) = (1 / 2)%R.
+Proof. easy. Qed.
+
+Lemma remove_q_2_r32 : Q2R (1 / 2) = (1 / 2)%R.
+Proof. easy. Qed.
+
+Lemma normalize_rotation1_2 : ((Z 1 1 (- (3 / 2 * PI))) ∝ (Z 1 1 (1 / 2 * PI))).
+Proof. apply (Z_simplify_general (-1)); lra. Qed.
+
+Lemma normalize_rotation3_2 : ((Z 1 1 (- (1 / 2 * PI))) ∝ (Z 1 1 (3 / 2 * PI))).
+Proof. apply (Z_simplify_general (-1)); lra. Qed.
+
+Local Hint Rewrite remove_q_2_r12 remove_q_2_r32 Ropp_0 : normalize_rotation_db.
+Local Hint Rewrite normalize_rotation1_2 normalize_rotation3_2 : normalize_rotation_db.
+
+Ltac normalize_rotation := autorewrite with normalize_rotation_db.
+
+(* fig 4 nam *)
+
+Lemma h_reduction_1 : RZH 0; @RZP 1 0; RZH 0 ≡u @RZPdag 1 0; RZH 0; RZPdag 0.
+Proof.
+  circuit_to_zx_full.
+  normalize_rotation.
+  apply h_p_reduction.
+Qed.
+
+Lemma h_reduction_2 : RZH 0; @RZPdag 1 0; RZH 0 ≡u @RZP 1 0; RZH 0; RZP 0.
+Proof.
+  circuit_to_zx_full.
+  apply conjugate_diagrams.
+  simpl.
+  normalize_rotation.
+  apply h_p_reduction.
+Qed.
+
+Lemma h_reduction_3 : @RZH 2 0; RZH 1; RZCNOT 0 1; RZH 0; RZH 1 ≡u RZCNOT 1 0.
+Proof.
+  circuit_to_zx_full.
+  rewrite compose_assoc.
+  rewrite <- (stack_compose_distr □ —).
+  cleanup_zx.
+  assert ((□ ↕ □) ∝ (2 ↑ □)) by (simpl; cleanup_zx; simpl_casts; easy).
+  rewrite H.
+  easy.
+Qed.
+
+Lemma h_p_reduction' : □ ⟷ Z 1 1 (1 / 2 * PI) ∝ Z 1 1 (3 / 2 * PI) ⟷ □ ⟷ Z 1 1 (3 / 2 * PI) ⟷ □.
+  rewrite <- h_p_reduction.
+  repeat rewrite compose_assoc.
+  cleanup_zx.
+  easy.
+Qed.
+
+Lemma h_reduction_4_5_zx : — ↕ □ ⟷ (— ↕ Z 1 1 ((1 / 2) * PI)) ⟷ (Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0))
+⟷ (— ↕ Z 1 1 ((3 / 2) * PI)) ⟷ (— ↕ □)
+∝ — ↕ Z 1 1 ((3 / 2) * PI) ⟷ (Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0))
+  ⟷ (— ↕ Z 1 1 ((1 / 2) * PI)).
+Proof.
+  repeat rewrite <- compose_assoc.
+  rewrite <- stack_compose_distr.
+  rewrite h_p_reduction'.
+  do 2 rewrite (compose_assoc (Z 1 1 (3 / 2 * PI))).
+  rewrite (compose_assoc □ _ □).
+  rewrite <- (nstack1_1 □) at 1 2.
+  rewrite <- colorswap_is_bihadamard.
+  simpl.
+  rewrite stack_compose_distr.
+  rewrite (compose_assoc _ (Z 1 2 0 ↕ —)).
+  rewrite cnot_is_cnot_r.
+  repeat rewrite <- compose_assoc.
+  rewrite (compose_assoc _ (— ↕ X 1 1 _)).
+  rewrite <- stack_compose_distr.
+  rewrite X_spider_1_1_fusion.
+  cleanup_zx.
+  rewrite (compose_assoc _ (—↕ X 1 2 _)).
+  rewrite <- cnot_is_cnot_r_general.
+  rewrite Rplus_0_r.
+  rewrite <- (Rplus_0_l (3 / 2 * PI)) at 2.
+  rewrite <- X_spider_1_1_fusion.
+  rewrite stack_wire_distribute_l.
+  replace (X 1 1 (3 / 2 * PI)) with (⊙(Z 1 1 (3 / 2 * PI))) by easy.
+  rewrite colorswap_is_bihadamard.
+  rewrite nstack1_1.
+  rewrite 2 stack_wire_distribute_l.
+  repeat rewrite compose_assoc.
+  rewrite <- 3 stack_wire_distribute_l.
+  rewrite <- (compose_assoc (Z 1 1 (3 / 2 * PI))).
+  rewrite <- (compose_assoc (Z 1 1 (3 / 2 * PI) ⟷ □)).
+  rewrite <- h_p_reduction'.
+  rewrite <- stack_wire_distribute_l. 
+  rewrite <- (compose_assoc □).
+  cleanup_zx.
+  easy.
+Qed.
+
+Lemma h_reduction_4 : @RZH 2 1; RZP 1; RZCNOT 0 1; RZPdag 1; RZH 1 ≡u RZPdag 1; RZCNOT 0 1; RZP 1.
+Proof.
+  circuit_to_zx_full.
+  normalize_rotation.
+  apply h_reduction_4_5_zx.
+Qed.
+
+Lemma h_reduction_5 : @RZH 2 1; RZPdag 1; RZCNOT 0 1; RZP 1; RZH 1 ≡u RZP 1; RZCNOT 0 1; RZPdag 1.
+Proof.
+  circuit_to_zx_full.
+  apply conjugate_diagrams.
+  simpl.
+  normalize_rotation.
+  apply h_reduction_4_5_zx.
+Qed.
+
+(* Fig 5 nam *)
+
+Lemma comm_1 : forall α, @RZRZ 2 α 1; RZH 1; RZCNOT 0 1; RZH 1 ≡u RZH 1; RZCNOT 0 1; RZH 1; RZRZ α 1.
+Proof.
+  intros.
+  circuit_to_zx_full.
+  assert ((Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0)) ∝ ⊙((X 1 2 0 ↕ — ⟷ (— ↕ Z 2 1 0)))) by (simpl; easy).
+  rewrite H.
+  rewrite colorswap_is_bihadamard.
+  simpl; cleanup_zx; simpl_casts.
+  repeat rewrite compose_assoc.
+  rewrite <- (compose_assoc (□ ↕ □) (— ↕ □)).
+  rewrite <- (stack_compose_distr □ —); cleanup_zx.
+  repeat rewrite <- compose_assoc.
+  rewrite (compose_assoc _ (— ↕ □)).
+  do 3 (rewrite <- (stack_compose_distr — □); cleanup_zx).
+  repeat rewrite compose_assoc.
+  do 2 rewrite <- (stack_compose_distr □ —); cleanup_zx.
+  rewrite <- (wire_removal_l □) at 4.
+  rewrite <- (wire_removal_r (Z 1 1 _)) at 2.
+  rewrite stack_compose_distr.
+  rewrite <- (compose_assoc (— ↕ (Z 2 1 0))).
+  rewrite <- stack_compose_distr.
+  rewrite Z_spider_1_1_fusion.
+  rewrite Rplus_0_l.
+  rewrite <- (Rplus_0_r (Q2R α * PI)) at 2.
+  rewrite <- Z_spider_1_1_fusion.
+  rewrite stack_compose_distr.
+  cleanup_zx.
+  bundle_wires.
+  cleanup_zx.
+  assert (□ ↕ Z 1 1 (Q2R α * PI) ⟷ (X 1 2 0 ↕ — ⟷ (— ↕ Z 2 1 0 ⟷ (□ ↕ —))) ∝ □ ↕ Z 1 1 (Q2R α * PI) ⟷ (X 1 2 0 ↕ — ⟷ (— ↕ Z 2 1 0) ⟷ (□ ↕ —))).
+  {
+    repeat rewrite compose_assoc.
+    easy.
+  }
+  rewrite H0; clear H0.
+  rewrite <- notc_is_notc_r.
+  repeat rewrite <- compose_assoc.
+  rewrite <- stack_compose_distr.
+  rewrite Z_spider_1_1_fusion.
+  rewrite Rplus_0_r.
+  rewrite <- (Rplus_0_l (Q2R α * PI)) at 1.
+  rewrite <- Z_spider_1_1_fusion.
+  rewrite stack_compose_distr.
+  cleanup_zx.
+  apply compose_simplify; try easy.
+  repeat rewrite compose_assoc.
+  apply compose_simplify; try easy.   
+  apply notc_is_notc_r_general.
+Qed.
+
+Lemma comm_2 : forall α β, @RZRZ 2 α 1; RZCNOT 0 1; RZRZ β 1; RZCNOT 0 1 ≡u  RZCNOT 0 1; RZRZ β 1; RZCNOT 0 1; RZRZ α 1.
+Proof.
+  intros.
+  circuit_to_zx_full.
+  solve_prop 1.
+Qed.
+
+Lemma comm_3 : forall α, @RZRZ 2 α 0; RZCNOT 0 1 ≡u RZCNOT 0 1; RZRZ α 0.
+Proof.
+  intros.
+  circuit_to_zx_full.
+  rewrite cnot_is_cnot_r at 2.
+  repeat rewrite <- compose_assoc.
+  rewrite <- (stack_compose_distr (Z 1 1 _) (Z 1 2 0) — —).
+  cleanup_zx.
+  rewrite Z_spider_1_1_fusion.
+  rewrite cnot_is_cnot_r_general.
+  repeat rewrite compose_assoc.
+  apply compose_simplify; [ easy | ].
+  rewrite <- (stack_compose_distr (Z 2 1 0) (Z 1 1 _) — —).
+  rewrite Z_spider_1_1_fusion.
+  cleanup_zx.
+  apply stack_simplify; [ | easy ].
+  apply Z_simplify.
+  lra.
+Qed.
+
+Lemma comm_4_5 : (— ↕ (□ ↕ □ ⟷ (Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0)) ⟷ (□ ↕ □))
+⟷ (Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0) ↕ —)
+∝ Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0) ↕ —
+  ⟷ (— ↕ (□ ↕ □ ⟷ (Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0)) ⟷ (□ ↕ □)))).
+Proof.
+  rewrite <- (nstack1_1 □).
+  rewrite <- nstack1_split.
+  rewrite compose_assoc.
+  rewrite <- (colorswap_is_bihadamard 2 2 _CNOT_).
+  simpl.
+  rewrite cnot_is_cnot_r at 1.
+  rewrite <- notc_is_notc_r at 1.
+  repeat rewrite stack_wire_distribute_l, stack_wire_distribute_r.
+  repeat rewrite <- compose_assoc.
+  rewrite (compose_assoc _ (— ↕ (X 2 1 0 ↕ —))).
+  rewrite (compose_assoc _ _ (— ↕ (X 1 2 0 ↕ —))).
+  rewrite 2 (stack_assoc_back — (X _ _ 0) —).
+  simpl_casts.
+  rewrite <- 2 (stack_compose_distr (— ↕ X 2 1 0) (— ↕ X 1 2 _) — —). 
+  rewrite <- (stack_compose_distr — — (X _ _ _)).
+  rewrite X_spider_1_1_fusion.
+  cleanup_zx.
+  rewrite X_wrap_over_top_right at 1.
+  rewrite stack_wire_distribute_l.
+  rewrite stack_wire_distribute_r.
+  repeat rewrite compose_assoc.
+  rewrite (stack_assoc_back — — (X 3 1 _)).
+  simpl_casts.
+  rewrite Rplus_0_r.
+  rewrite <- (stack_wire_distribute_r (— ↕ — ↕ X 3 1 0) (Z 2 1 0 ↕ —)).
+  rewrite <- (stack_compose_distr (— ↕ —) (Z 2 1 _) (X 3 1 0) —).
+  bundle_wires.
+  cleanup_zx.
+  rewrite <- (stack_wire_distribute_r (— ↕ (⊂ ↕ n_wire 2)) (Z 2 1 0 ↕ X 3 1 0)).
+  rewrite <- (nstack1_1 —) at 3.
+  rewrite <- (nwire_stack_compose_botleft (Z 2 1 0)).
+  repeat rewrite <- compose_assoc.
+  rewrite <- (n_wire_stack 1 2).
+  rewrite stack_assoc_back.
+  rewrite (stack_assoc_back _ (n_wire 1) (n_wire 2)).
+  simpl_casts.
+  rewrite <- (stack_nwire_distribute_r (n_wire 1 ↕ ⊂) (Z 2 1 0 ↕ n_wire 1)).
+  rewrite nstack1_1 at 2.
+  assert (forall prfn prfm, n_wire 1 ↕ ⊂ ∝ (cast 1 (1 + 1 + 1) prfn prfm (n_wire 1 ↕ ⊂))) as Hcast1. { intros; simpl_casts. easy. }
+  rewrite Hcast1; clear Hcast1.
+  rewrite <- (Z_wrap_under_bot_left 1).
+  rewrite stack_wire_distribute_r.
+  repeat rewrite <- compose_assoc.
+  rewrite (stack_assoc (Z 1 2 _) (n_wire 2) —); simpl_casts.
+  rewrite <- (stack_compose_distr — (Z 1 2 _) (— ↕  _) (n_wire 2 ↕ —)).
+  rewrite wire_removal_l.
+  rewrite <- (nwire_removal_r (Z 1 2 0)) at 1.
+  rewrite stack_compose_distr.
+  rewrite <- (nwire_stack_compose_botleft (Z 1 2 0)).
+  repeat rewrite compose_assoc.
+  apply compose_simplify; [ zx_simpl; rewrite stack_assoc_back; simpl_casts; easy | ].
+  bundle_wires.
+  cleanup_zx.
+  rewrite (X_wrap_under_bot_right 2).
+  simpl_casts.
+  rewrite stack_wire_distribute_l, stack_wire_distribute_r.
+  rewrite stack_assoc_back; simpl_casts.
+  rewrite (stack_assoc_back — (X 2 2 _ ) —); simpl_casts.
+  rewrite (stack_assoc (— ↕ (X 2 2 _))); simpl_casts. 
+  repeat rewrite <- compose_assoc.
+  rewrite <- (stack_compose_distr (n_wire 2 ↕ —) (— ↕ X 2 2 0) (Z 1 2 0) (— ↕ —)).
+  bundle_wires.
+  cleanup_zx.
+  rewrite <- (nwire_stack_compose_botleft (— ↕ X 2 2 _) (Z _ _ _)).
+  repeat rewrite compose_assoc.
+  repeat rewrite stack_assoc; simpl_casts.
+  apply compose_simplify; [ rewrite nstack1_1; easy | ].
+  rewrite <- n_wire_stack.
+  rewrite <- (n_wire_stack 1 1).
+  repeat rewrite stack_assoc; simpl_casts.
+  rewrite nstack1_1.
+  rewrite <- (stack_wire_distribute_l (— ↕ — ↕ Z 1 (1 + 1) 0)).
+  apply stack_simplify; [ easy | ].
+  rewrite stack_assoc; simpl_casts.
+  rewrite (stack_assoc — ⊃ —); simpl_casts.
+  rewrite <- (stack_wire_distribute_l (— ↕ Z 1 (1 + 1) 0) (⊃ ↕ —)).
+  apply stack_simplify; [ easy | ].
+  rewrite <- (nstack1_1 —) at 2.
+  rewrite <- Z_wrap_over_top_left.
+  easy. 
+Unshelve.
+  all: lia.
+Qed.
+
+Lemma comm_4 : @RZCNOT 3 2 1; RZCNOT 0 1 ≡u RZCNOT 0 1; RZCNOT 2 1.
+Proof.
+  circuit_to_zx_full.
+  apply comm_4_5.
+Qed.
+
+Lemma comm_5 : @RZCNOT 3 1 2; RZCNOT 1 0 ≡u RZCNOT 1 0; RZCNOT 1 2.
+Proof.
+  circuit_to_zx_full.
+  apply colorswap_diagrams.
+  simpl.
+  assert (X 1 2 0 ↕ — ⟷ (— ↕ Z 2 1 0) ∝ □ ↕ □ ⟷ (Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0)) ⟷ (□ ↕ □)).
+  {
+    rewrite <- (nstack1_1 □).
+    rewrite <- nstack1_split.
+    rewrite compose_assoc.
+    rewrite <- colorswap_is_bihadamard.
+    simpl.
+    easy.
+  }
+  assert (□ ↕ □ ⟷ (X 1 2 0 ↕ — ⟷ (— ↕ Z 2 1 0)) ⟷ (□ ↕ □) ∝ (Z 1 2 0 ↕ — ⟷ (— ↕ X 2 1 0))).
+  {
+    rewrite <- (nstack1_1 □).
+      rewrite <- nstack1_split.
+      rewrite compose_assoc.
+      rewrite <- colorswap_is_bihadamard.
+      simpl.
+      easy.
+  }
+  rewrite H at 1.
+  rewrite H0 at 1.
+  rewrite comm_4_5.
+  apply compose_simplify; apply stack_simplify; easy.
+Qed.
+
+Lemma comm_6 : @RZCNOT 3 0 1; RZH 1; RZCNOT 1 2; RZH 1 ≡u RZH 1; RZCNOT 1 2; RZH 1; RZCNOT 0 1.
+Proof.
+  circuit_to_zx_full.
+  repeat rewrite compose_assoc.
+  rewrite (stack_assoc — □ —); simpl_casts.
+  rewrite <- (stack_wire_distribute_l _CNOT_ (□ ↕ —)).
+  rewrite <- stack_wire_distribute_l.
+  rewrite compose_assoc.
+  rewrite <- (stack_compose_distr — □ (X 2 1 0)).
+  cleanup_zx.
+  rewrite <- (nwire_stack_compose_botleft □ (X 2 1 0)).
+  rewrite <- (compose_assoc (Z 1 2 0 ↕ —)).
+  rewrite <- (nstack1_1 —) at 6.
+  replace (Z 1 2 0) with (⊙ (X 1 2 0)) at 2 by easy.
+  rewrite colorswap_is_bihadamard.
+  zx_simpl.
+  repeat rewrite <- compose_assoc.
+  rewrite <- (stack_wire_distribute_r □ (□ ⟷ X 1 2 0 ⟷ (□ ↕ □))).
+  repeat rewrite <- compose_assoc.
+  cleanup_zx.
+  rewrite (stack_assoc_back □ — —); simpl_casts.
+  rewrite <- (stack_wire_distribute_r (X 1 2 0 ⟷ (□ ↕ □)) (□ ↕ —)).
+  rewrite (compose_assoc (X 1 2 0)).
+  rewrite <- (stack_compose_distr □ □ □).
+  cleanup_zx.
+  rewrite (stack_wire_distribute_r (Z 1 2 0 ↕ —) (— ↕ X 2 1 0)) at 1.
+  rewrite stack_wire_distribute_l.
+  repeat rewrite compose_assoc.
+  rewrite <- (compose_assoc (— ↕ X 2 1 0 ↕ —)).
+  rewrite (stack_assoc — (X 2 1 0) —); simpl_casts.
+  rewrite <- (stack_wire_distribute_l (X 2 1 0 ↕ —)).
+  rewrite <- (stack_wire_distribute_r (X 2 1 0) (X 1 2 0 ⟷ (— ↕ □))).
+  rewrite <- compose_assoc.
+  rewrite X_spider_1_1_fusion.
+  rewrite X_wrap_over_top_left.
+  repeat (rewrite stack_wire_distribute_r; rewrite stack_wire_distribute_l).
+  repeat rewrite <- compose_assoc.
+  rewrite (stack_assoc (Z 1 2 0)).
+  rewrite (stack_assoc_back —).
+  simpl_casts.
+  rewrite Rplus_0_l.
+  rewrite (stack_assoc_back — —  (X 1 3 0)); simpl_casts.
+  rewrite (stack_assoc (— ↕ —)); simpl_casts.
+  rewrite <- (stack_compose_distr (Z 1 2 0) (— ↕ —) (— ↕ —) (X 1 3 0 ↕ —)).
+  bundle_wires; cleanup_zx.
+  rewrite <- (nwire_stack_compose_topleft (X 1 3 0 ↕ —)).
+  repeat rewrite <- compose_assoc.
+  rewrite (compose_assoc (n_wire 1 ↕ (X 1 3 0 ↕ —))).
+  rewrite <- (n_wire_stack 1 3).
+  rewrite (stack_assoc_back — _ —).
+  rewrite (stack_assoc_back — ⊃ (n_wire 2)).
+  rewrite (stack_assoc_back (Z 1 2 0) (n_wire 1) (n_wire 3)).
+  simpl_casts.
+  rewrite (stack_assoc (— ↕ ⊃) (n_wire 2) —); simpl_casts.
+  rewrite <- (stack_compose_distr (Z 1 2 0 ↕ n_wire 1) (— ↕ ⊃) (n_wire 3) (n_wire 2 ↕ —)).
+  assert (forall prfn prfm, (— ↕ ⊃) ∝ cast (1 + 1 + 1) 1 prfn prfm (n_wire 1 ↕ ⊃)) as Hcast1 by (intros; zx_simpl; easy).
+  rewrite Hcast1.
+  rewrite nstack1_1 at 2.
+  rewrite <- (Z_wrap_under_bot_right 1 1 0).
+  rewrite <- (nstack1_1 —) at 5.
+  cleanup_zx.
+  rewrite (X_add_r_base_rot 2 1).
+  cleanup_zx.
+  rewrite stack_wire_distribute_r.
+  rewrite stack_nwire_distribute_l.
+  rewrite (stack_assoc — □ —).
+  rewrite (stack_assoc_back — —).
+  simpl_casts.
+  rewrite (stack_assoc_back — — (□ ↕ —)); simpl_casts.
+  rewrite <- (n_wire_stack 1 1).
+  rewrite nstack1_1.
+  rewrite (stack_assoc — — —). 
+  rewrite (stack_assoc (X 1 2 0) — —).
+  simpl_casts.
+  rewrite (stack_assoc_back (Z 2 1 0) —).
+  rewrite (stack_assoc_back — (X 1 2 0) (— ↕ —)).
+  simpl_casts.
+  repeat rewrite compose_assoc.
+  rewrite <- (stack_compose_distr (— ↕ —) (— ↕ —) (□ ↕ —) (X 2 1 0)).
+  rewrite <- (stack_compose_distr (Z 2 1 0 ↕ —) (— ↕ — ⟷ (— ↕ —)) (— ↕ —) (□ ↕ — ⟷ X 2 1 0)).
+  rewrite <- (stack_compose_distr (— ↕ X 1 2 0) (Z 2 1 0 ↕ — ⟷ (— ↕ — ⟷ (— ↕ —))) (— ↕ —) (— ↕ — ⟷ (□ ↕ — ⟷ X 2 1 0))).
+  bundle_wires.
+  cleanup_zx.
+  rewrite <- cnot_is_cnot_r.
+  replace (Z 1 2 0) with (⊙ (X 1 2 0)) at 2 by easy.
+  rewrite colorswap_is_bihadamard.
+  zx_simpl.
+  repeat rewrite <- compose_assoc.
+  rewrite <- stack_wire_distribute_l.
+  rewrite <- (stack_wire_distribute_r □ (□ ⟷ X 1 2 0 ⟷ (□ ↕ □))).
+  repeat rewrite <- compose_assoc.
+  cleanup_zx.
+  rewrite (stack_assoc — —); simpl_casts.
+  rewrite stack_wire_distribute_r.
+  rewrite stack_wire_distribute_l.
+  repeat rewrite <- compose_assoc.
+  rewrite 2 (compose_assoc (— ↕ (X 1 2 0 ↕ —))).
+  rewrite <- 2 stack_wire_distribute_l.
+  rewrite (stack_assoc □); simpl_casts.
+  rewrite <- (stack_compose_distr □ — (□ ↕ —)).
+  rewrite wire_removal_r.
+  rewrite <- (stack_compose_distr □ □ (□ ↕ — ⟷ X 2 1 0)).
+  cleanup_zx.
+  repeat rewrite compose_assoc.
+  apply compose_simplify; [ easy | ].
+  rewrite 2 stack_wire_distribute_l.
+  rewrite (stack_assoc_back — —).
+  rewrite (stack_assoc_back — — (□ ↕ —)).
+  simpl_casts.
+  rewrite <- (stack_compose_distr (— ↕ —) (— ↕ —) (□ ↕ —) (X 2 1 0)).
+  rewrite <- (nstack1_1 —) at 4 5 6 7.
+  rewrite n_wire_stack.
+  cleanup_zx.
+  rewrite <- (stack_wire_distribute_r (Z 1 2 0 ↕ —) (— ↕ X 2 1 0)).
+  rewrite <- (nstack1_1 —) at 8.
+  rewrite (nwire_stack_compose_topleft (□ ↕ — ⟷ X 2 1 0) _CNOT_).
+  easy.
+Unshelve.
+all: lia.
+Qed.
+
+
+
diff --git a/src/Ingest/SQIRIngest.v b/src/Ingest/SQIRIngest.v
index 894bf88..c36294c 100644
--- a/src/Ingest/SQIRIngest.v
+++ b/src/Ingest/SQIRIngest.v
@@ -1,2 +1,4 @@
 From VyZX Require Export Ingest.
-From VyZX Require Export ZXPad.
\ No newline at end of file
+From VyZX Require Export ZXPad.
+From VyZX Require Export Interact.
+