diff --git a/src/library/blast/simplifier/ceqv.cpp b/src/library/blast/simplifier/ceqv.cpp
index 4c0d0f36e6..2123c7b126 100644
--- a/src/library/blast/simplifier/ceqv.cpp
+++ b/src/library/blast/simplifier/ceqv.cpp
@@ -207,9 +207,9 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
             return lhs == rhs; // locally bound variable
         } else if (var_idx(lhs) - offset < p.size()) {
             if (p[var_idx(lhs) - offset]) {
-                return *(p[var_idx(lhs) - offset]) == var_idx(rhs);
+                return *(p[var_idx(lhs) - offset]) == var_idx(rhs) - offset;
             } else {
-                p[var_idx(lhs) - offset] = var_idx(rhs);
+                p[var_idx(lhs) - offset] = var_idx(rhs) - offset;
                 return true;
             }
         } else {
diff --git a/tests/lean/run/perm_with_pi_args.lean b/tests/lean/run/perm_with_pi_args.lean
new file mode 100644
index 0000000000..9370c22a6a
--- /dev/null
+++ b/tests/lean/run/perm_with_pi_args.lean
@@ -0,0 +1,6 @@
+import data.matrix data.real data.fin
+open matrix real
+
+axiom mx_add_comm {m n} (M₁ M₂ : matrix ℝ m n) : M₁ + M₂ = M₂ + M₁
+attribute mx_add_comm [simp]
+example (m n : ℕ) (M₁ M₂ : matrix ℝ m n) : M₁ + M₂ = M₂ + M₁ := by simp