diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 79a960d14..416bb493c 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -1208,7 +1208,7 @@ class rewrite_fn {
             level l2 = sort_level(m_tc->ensure_type(A).first);
             expr H;
             if (has_dep_elim) {
-                expr Haeqx = mk_app(mk_constant(get_eq_name(), {l1}), A, b, mk_var(0));
+                expr Haeqx = mk_app(mk_constant(get_eq_name(), {l1}), A, a, mk_var(0));
                 expr P     = mk_lambda("x", A, mk_lambda("H", Haeqx, Px));
                 H          = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, a, P, hyp, b, Heq});
             } else {