diff --git a/zkvm/docs/zkvm-spec.md b/zkvm/docs/zkvm-spec.md
index de36076e7..4b25673f5 100644
--- a/zkvm/docs/zkvm-spec.md
+++ b/zkvm/docs/zkvm-spec.md
@@ -1368,6 +1368,7 @@ _constr_ **verify** → ø
 2. Transforms the constraint `constr` recursively using the following rules:
     1. Replace conjunction of two _linear constraints_ `a` and `b` with a linear constraint `c` by combining both constraints with a random challenge `z`:
         ```
+        z = transcript.challenge_scalar(b"ZkVM.verify.and-challenge");
         c = a + z·b
         ```
     2. Replace disjunction of two _linear constraints_ `a` and `b` by constrainting an output `o` of a newly allocated multiplier `{r,l,o}` to zero, while adding constraints `r == a` and `l == b` to the constraint system.
diff --git a/zkvm/src/constraints.rs b/zkvm/src/constraints.rs
index 2d8f74838..dd7c77daa 100644
--- a/zkvm/src/constraints.rs
+++ b/zkvm/src/constraints.rs
@@ -257,14 +257,6 @@ impl Add for Expression {
     }
 }
 
-impl Sub for Expression {
-    type Output = Expression;
-
-    fn sub(self, rhs: Expression) -> Expression {
-        self + -rhs
-    }
-}
-
 // Upcasting witness/points into Commitment
 
 impl From<CommitmentWitness> for Commitment {