diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 413a028..49704c4 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -12,11 +12,10 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.14'
-          - '8.15'
           - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev'
         ocaml_version:
           - 'default'
diff --git a/README.md b/README.md
index 3eea313..8d418ea 100644
--- a/README.md
+++ b/README.md
@@ -6,10 +6,18 @@
 
 ## Building ViCAR
 
-Tested with Coq 8.14-8.18.
+Currently supports Coq 8.16-8.19.
 
-To build ViCaR, run `make vicar`
+To build ViCaR, run `make vicar`.
 
+## Installing ViCAR through opam
+
+To install ViCAR through opam, run 
+```bash
+opam pin -y coq-vicar https://github.com/inQWIRE/ViCAR.git
+```
+
+To use the visualizer, first have [coq-lsp](https://github.com/ejgallego/coq-lsp) installed, then install the VSCode extension found at [https://marketplace.visualstudio.com/items?itemName=inQWIRE.vizcar]. After instantiating the appropriate typeclass you would like to visualize you can run the vizcar command in vscode to activate visualizing. The vizcar plugin only visualizes terms using the ViCAR grammar. To automatically take a term with an instantiated typeclass to the ViCAR grammar, use the `to_Cat` tactic.
 
 ## Examples
 
diff --git a/ViCaR/Classes/BraidedMonoidal.v b/ViCaR/Classes/BraidedMonoidal.v
index 46d1d37..392d155 100644
--- a/ViCaR/Classes/BraidedMonoidal.v
+++ b/ViCaR/Classes/BraidedMonoidal.v
@@ -67,13 +67,15 @@ Lemma hexagon_resultant_1 (A B M : C) :
   id_ B ⊗ β_ M, A ∘ β_ B, (A×M) ∘ associator A M B ∘ id_ A ⊗ (β_ B, M)^-1
   ≃ associator B M A ^-1 ∘ β_ (B × M), A.
 Proof.
-  (* rewrite <- compose_iso_l. *)
   pose proof (hexagon_2 A B M) as hex2.
-  rewrite <- (compose_tensor_iso_r' _ (IdentityIsomorphism _)).
+  replace (id_ A) with (IdentityIsomorphism A ^-1) by easy.
+  rewrite <- (compose_tensor_iso_r' (associator B M A ^-1 ∘ β_ B × M, A) (IdentityIsomorphism A) (β_ B, M)).
   simpl.
   rewrite 2!compose_iso_r.
   rewrite !(assoc).
   rewrite <- compose_iso_l.
+  Check compose_tensor_iso_r.
+  replace (id_ B) with (forward (IdentityIsomorphism B)) by easy.
   rewrite (compose_tensor_iso_r _ (IdentityIsomorphism _)).
   rewrite (assoc), compose_iso_l'.
   symmetry in hex2.
@@ -85,6 +87,7 @@ Proof.
   apply compose_cancel_r.
   pose proof (hexagon_1 B A M) as hex1.
   rewrite assoc, <- compose_iso_l'.
+  replace (id_ M) with (IdentityIsomorphism M ^-1) by easy.
   rewrite <- (compose_tensor_iso_l' _ (IdentityIsomorphism _)).
   simpl.
   rewrite <- 3!(assoc).
@@ -95,5 +98,4 @@ Qed.
 
 End BraidedCoherenceRewrites.
 
-
-Local Close Scope Cat.
\ No newline at end of file
+Local Close Scope Cat.
diff --git a/coq-vicar.opam b/coq-vicar.opam
index b630cfb..72db620 100644
--- a/coq-vicar.opam
+++ b/coq-vicar.opam
@@ -1,19 +1,19 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.1.0"
+version: "0.1.1"
 synopsis: "Coq library reasoning about categorical string diagrams"
 description: """
-inQWIRE's ViCaR is a library for reasoning about
+inQWIRE's ViCAR is a library for reasoning about
  categorical string diagrams
 """
 maintainer: ["inQWIRE Developers"]
 authors: ["inQWIRE"]
 license: "MIT"
-homepage: "https://github.com/inQWIRE/ViCaR"
-bug-reports: "https://github.com/inQWIRE/ViCaR/issues"
+homepage: "https://github.com/inQWIRE/ViCAR"
+bug-reports: "https://github.com/inQWIRE/ViCAR/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq" {>= "8.12"}
+  "coq" {>= "8.16"}
   "odoc" {with-doc}
 ]
 build: [
@@ -30,4 +30,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/inQWIRE/ViCaR.git"
+dev-repo: "git+https://github.com/inQWIRE/ViCAR.git"
diff --git a/dune-project b/dune-project
index a57ea96..c9f0a92 100644
--- a/dune-project
+++ b/dune-project
@@ -18,4 +18,4 @@
  )
 
  (depends
-   (coq (>= 8.12))))
+   (coq (>= 8.16))))