diff --git a/SQIR/UnitaryOps.v b/SQIR/UnitaryOps.v
index 5f5e84b..f6f1d69 100644
--- a/SQIR/UnitaryOps.v
+++ b/SQIR/UnitaryOps.v
@@ -1,5 +1,5 @@
 Require Export UnitarySem.
-Require Export QuantumLib.VectorStates.
+Require Export QuantumLib.VectorStates QuantumLib.Bits.
 
 (* This file contains useful operations over unitary programs including:
    - inversion
diff --git a/VOQC/RemoveZRotationBeforeMeasure.v b/VOQC/RemoveZRotationBeforeMeasure.v
index b6c2805..d494028 100644
--- a/VOQC/RemoveZRotationBeforeMeasure.v
+++ b/VOQC/RemoveZRotationBeforeMeasure.v
@@ -81,6 +81,9 @@ Proof.
   repeat rewrite Mmult_assoc.
   Msimpl.
   repeat (restore_dims; rewrite <- Mmult_assoc).
+  (* This line is extraneous with the patch to 
+     Qsimpl / Q_db in QuantumLib > 1.5.0 *)
+  replace (σx †) with σx by (symmetry; apply σx_hermitian).
   Qsimpl.
   rewrite Mplus_comm; reflexivity.
   rewrite Mplus_comm; reflexivity.
diff --git a/coq-sqir.opam b/coq-sqir.opam
index 617d0f8..3efcd97 100644
--- a/coq-sqir.opam
+++ b/coq-sqir.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.3.0"
+version: "1.3.1"
 synopsis: "Coq library for reasoning about quantum circuits"
 description: """
 inQWIRE's SQIR is a Coq library for reasoning
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "3.8"}
   "coq-interval" {>= "4.9.0"}
-  "coq-quantumlib" {= "1.3.0"}
+  "coq-quantumlib" {>= "1.5.0"}
   "coq" {>= "8.16"}
   "odoc" {with-doc}
 ]
diff --git a/coq-voqc.opam b/coq-voqc.opam
index c9eca2d..b53d2f0 100644
--- a/coq-voqc.opam
+++ b/coq-voqc.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.3.0"
+version: "1.3.1"
 synopsis: "A verified optimizer for quantum compilation"
 description: """
 inQWIRE's VOQC is a Coq library for verified
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "2.8"}
   "coq-interval" {>= "4.6.1"}
-  "coq-quantumlib" {>= "1.1.0" < "1.4.0"}
+  "coq-quantumlib" {>= "1.1.0"}
   "coq-sqir" {>= "1.3.0"}
   "coq" {>= "8.12"}
   "odoc" {with-doc}
diff --git a/dune-project b/dune-project
index 81e4a85..40c50a4 100644
--- a/dune-project
+++ b/dune-project
@@ -1,6 +1,6 @@
 (lang dune 3.8)
 (name coq-sqirvoqc)
-(version 1.3.0)
+(version 1.3.1)
 (using coq 0.7)
 (generate_opam_files true)
 
@@ -17,7 +17,7 @@
  )
  (depends
    (coq-interval (>= 4.9.0))
-   (coq-quantumlib (= 1.3.0))
+   (coq-quantumlib (>= 1.5.0))
    (coq (>= 8.16))))
 
 (package
@@ -28,6 +28,6 @@
  )
  (depends
    (coq-interval (>= 4.9.0))
-   (coq-quantumlib (>= 1.3.0))
+   (coq-quantumlib (>= 1.5.0))
    (coq-sqir (>= 1.3.0))
    (coq (>= 8.16))))