diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean
index 33cdfcd074..7af421523e 100644
--- a/library/init/meta/contradiction_tactic.lean
+++ b/library/init/meta/contradiction_tactic.lean
@@ -34,7 +34,7 @@ private meta def contra_false : list expr → tactic unit
 private meta def contra_not_a_refl_rel_a : list expr → tactic unit
 | []        := failed
 | (H :: Hs) :=
-  do t ← infer_type H,
+  do t ← infer_type H >>= beta,
      (do (lhs, rhs) ← match_ne t,
          unify lhs rhs,
          tgt ← target,
diff --git a/tests/lean/run/contradiction_issue.lean b/tests/lean/run/contradiction_issue.lean
new file mode 100644
index 0000000000..2fdb1bd81b
--- /dev/null
+++ b/tests/lean/run/contradiction_issue.lean
@@ -0,0 +1,5 @@
+open tactic
+
+def hd {α} : {l : list α // l ≠ []} → α
+| ⟨[],   h⟩ := by contradiction
+| ⟨a::l, h⟩ := a