diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp
index d2cfaf2454..11d48a84d3 100644
--- a/src/library/constructions/injective.cpp
+++ b/src/library/constructions/injective.cpp
@@ -157,8 +157,12 @@ expr prove_injective(environment const & env, expr const & inj_type, name const
     while (is_pi(ty)) {
         expr eq = tctx.push_local_from_binding(ty);
         eqs.push_back(eq);
-        if (app_arg(tctx.infer(eq)) != app_arg(app_fn(tctx.infer(eq))))
+        expr eq_type = tctx.infer(eq);
+        expr lhs, rhs;
+        if ((is_eq(eq_type, lhs, rhs) && lhs != rhs) ||
+            (is_heq(eq_type, lhs, rhs) && lhs != rhs)) {
             eqs_to_keep.push_back(eq);
+        }
         ty = tctx.relaxed_whnf(instantiate(binding_body(ty), eq));
     }
 
@@ -253,7 +257,7 @@ environment mk_injective_lemmas(environment const & _env, name const & ind_name)
         expr ir_type = inductive::intro_rule_type(ir);
         expr inj_type = mk_injective_type(env, ir_name, ir_type, num_params, lp_names);
         expr inj_val = prove_injective(env, inj_type, ind_name);
-        lean_trace(name({"constructions", "injective"}), tout() << ir_name << " : " << inj_type << " :=\n  " << inj_val;);
+        lean_trace(name({"constructions", "injective"}), tout() << ir_name << " : " << inj_type << " :=\n  " << inj_val << "\n";);
         env = module::add(env, check(env, mk_definition_inferring_trusted(env, mk_injective_name(ir_name), lp_names, inj_type, inj_val, true)));
         env = mk_injective_arrow(env, ir_name);
     }
diff --git a/tests/lean/run/1609.lean b/tests/lean/run/1609.lean
new file mode 100644
index 0000000000..c80d9ef656
--- /dev/null
+++ b/tests/lean/run/1609.lean
@@ -0,0 +1,4 @@
+universe variable u
+
+inductive pred : ∀ (X : Type u), list X → Type (u+1)
+| foo X (l1 : list X) (l2 : list (option X)) : pred (option X) l2 → pred X l1