diff --git a/intTests/test2009/test.saw b/intTests/test2009/test.saw
new file mode 100644
index 0000000000..f4c5adc448
--- /dev/null
+++ b/intTests/test2009/test.saw
@@ -0,0 +1,4 @@
+let pairEq = parse_core "pairEq (Vec 32 Bool) (Vec 32 Bool) (bvEq 32) (bvEq 32)";
+t <- prove_print w4 {{ \x -> pairEq (x, x + 1) (x, 1 + x) }};
+print_term (rewrite (addsimp t empty_ss) {{ (0 : [32], 0 + 1 : [32]) }});
+
diff --git a/intTests/test2009/test.sh b/intTests/test2009/test.sh
new file mode 100644
index 0000000000..d0c501894a
--- /dev/null
+++ b/intTests/test2009/test.sh
@@ -0,0 +1,4 @@
+set -e
+
+$SAW test.saw
+
diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index 92fb67eb54..6500347363 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -326,6 +326,9 @@ boolEqIdent = mkIdent (mkModuleName ["Prelude"]) "boolEq"
 vecEqIdent :: Ident
 vecEqIdent = mkIdent (mkModuleName ["Prelude"]) "vecEq"
 
+pairEqIdent :: Ident
+pairEqIdent = mkIdent (mkModuleName ["Prelude"]) "pairEq"
+
 arrayEqIdent :: Ident
 arrayEqIdent = mkIdent (mkModuleName ["Prelude"]) "arrayEq"
 
@@ -394,6 +397,7 @@ ruleOfProp sc term ann =
     (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) -> eqRule x y
     (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) -> eqRule x y
     (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef pairEqIdent -> Just (), [_, _, _, _, x, y])) -> eqRule x y
     (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) -> eqRule x y
     (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) -> eqRule x y
     (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) -> eqRule x y