diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index a02f0bdbcec..e8278bb68d6 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -996,6 +996,20 @@ void BasicBlockConstraintMap::approximateAndInternal(Index index,
   }
 }
 
+Result BasicBlockConstraintMap::proves(LocalConstraint condition) const {
+  // As in approximateAnd, above, if the term is a local that we know something
+  // about, propagate it. TODO: even without equality, we can add more
+  // constraints here (e.g. x < y and y < 10 can lead to proving x < 10)
+  if (auto* other = std::get_if<Index>(&condition.constraint.term)) {
+    auto otherConstraints = get(*other);
+    if (auto lit = otherConstraints.getLiteral()) {
+      condition.constraint.term = Term{*lit};
+    }
+  }
+
+  return get(condition.local).proves(condition.constraint);
+}
+
 void BasicBlockConstraintMap::noteRefs(Index index, const Constraint& c) {
   if (auto* i = std::get_if<Index>(&c.term)) {
     refs[*i].insert(index);
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index ced8edd0b46..688aef53421 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -319,9 +319,8 @@ struct BasicBlockConstraintMap {
     approximateAndInternal(index, c);
   }
 
-  // TODO: Add proves() here, which could do things like: if asked x == y, we
-  // can answer False if we see x == c1, y == c2, and the constants c1, c2
-  // differ.
+  // Check a condition on a local, given all we know about all other locals.
+  Result proves(LocalConstraint condition) const;
 
   bool operator!=(const BasicBlockConstraintMap& other) {
     return unreachable != other.unreachable || map != other.map;
diff --git a/src/passes/ConstraintAnalysis.cpp b/src/passes/ConstraintAnalysis.cpp
index aaf9243ec69..f1b04cb5a79 100644
--- a/src/passes/ConstraintAnalysis.cpp
+++ b/src/passes/ConstraintAnalysis.cpp
@@ -439,8 +439,7 @@ struct ConstraintAnalysis
       return;
     }
 
-    auto localConstraints = constraints.get(parsed->local);
-    Result result = localConstraints.proves(parsed->constraint);
+    auto result = constraints.proves(*parsed);
     if (result == Unknown) {
       // If we parsed something using two locals, like x != y, we can also look
       // for the flipped condition among y's constraints TODO
diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index cbec8495f43..9c1e594f18e 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -1526,10 +1526,7 @@
   ;; CHECK-NEXT:  (local $y i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (br_if $loop
-  ;; CHECK-NEXT:    (i32.lt_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (local.get $y)
-  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (i32.const 0)
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
@@ -1538,7 +1535,8 @@
     (local $y i32)
     (loop $loop
       ;; x == y == 0, so x < y leads to a contradiction, and we never branch
-      ;; back up to the loop. We should not error here.
+      ;; back up to the loop. We should not error here, and in fact infer a 0
+      ;; for this condition.
       (br_if $loop
         (i32.lt_s
           (local.get $x)
@@ -1553,10 +1551,7 @@
   ;; CHECK-NEXT:  (local $y i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (br_if $loop
-  ;; CHECK-NEXT:    (i32.lt_u
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (local.get $y)
-  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (i32.const 0)
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 46a9058a130..93f84f4d18c 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -1483,10 +1483,7 @@
   ;; CHECK-NEXT:   (i32.const 1)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT:  (if
-  ;; CHECK-NEXT:   (i32.eq
-  ;; CHECK-NEXT:    (local.get $y)
-  ;; CHECK-NEXT:    (local.get $x)
-  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (i32.const 0)
   ;; CHECK-NEXT:   (then
   ;; CHECK-NEXT:    (drop
   ;; CHECK-NEXT:     (unreachable)
@@ -1501,10 +1498,7 @@
   ;; OPTIN-NEXT:   (i32.const 1)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (if
-  ;; OPTIN-NEXT:   (i32.eq
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (local.get $y)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 0)
   ;; OPTIN-NEXT:   (then
   ;; OPTIN-NEXT:    (drop
   ;; OPTIN-NEXT:     (unreachable)
@@ -1521,7 +1515,8 @@
     ;; $x == 0, $y == 1, so they are never equal, and the if body is
     ;; unreachable. We find this out while applying the secondary facts of a
     ;; constraint: we add $y == $x, and then apply $x's constraints to $y,
-    ;; ending up in $y with $y == 1 && $y == 0.
+    ;; ending up in $y with $y == 1 && $y == 0. We can also infer 0 for the if
+    ;; condition.
     (if
       (i32.eq
         (local.get $y)
@@ -4722,10 +4717,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT:  (drop
-  ;; CHECK-NEXT:   (i32.eq
-  ;; CHECK-NEXT:    (local.get $x)
-  ;; CHECK-NEXT:    (local.get $w)
-  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (i32.const 0)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
   ;; OPTIN:      (func $fallthrough-get (type $1)
@@ -4746,10 +4738,7 @@
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.eq
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (local.get $w)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 0)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
   (func $fallthrough-get
@@ -4777,8 +4766,7 @@
 
     ;; 0 == 42 is 0 at runtime. If we did not mark $z as relevant, we would see
     ;; $x and $w as both equal to $z, i.e., that they are themselves equal, and
-    ;; misoptimize this to 1. The actual value at runtime is 0.
-    ;; TODO: actually optimize this to 0
+    ;; misoptimize this to 1. We optimize to 0 here.
     (drop
       (i32.eq
         (local.get $x)
@@ -4805,10 +4793,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT:  (drop
-  ;; CHECK-NEXT:   (i32.eq
-  ;; CHECK-NEXT:    (local.get $x)
-  ;; CHECK-NEXT:    (local.get $w)
-  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (i32.const 0)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
   ;; OPTIN:      (func $fallthrough-tee (type $0) (param $param i32)
@@ -4829,10 +4814,7 @@
   ;; OPTIN-NEXT:   )
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.eq
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (local.get $w)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 0)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
   (func $fallthrough-tee (param $param i32)
@@ -4854,8 +4836,7 @@
       )
     )
 
-    ;; As before, this should not be optimized to 1, and could be optimized to
-    ;; 0 (TODO).
+    ;; As before, this is optimized to 0.
     (drop
       (i32.eq
         (local.get $x)