fix: fixes #1549

src/Lean/Meta/DiscrTree.lean

@@ -478,6 +478,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
       match k with
       | Key.star  => return result
       /-
+        Note: dep-arrow vs arrow
         Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are `(Key.arrow, #[a, b])`.
         A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`). Thus, we also visit the `Key.other` child.
       -/
@@ -494,8 +495,10 @@ private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α)
     let result := getStarResult d
     let (k, args) ← getMatchKeyArgs e (root := true)
     match k with
-    | Key.star => return (k, result)
-    | _        => return (k, ← getMatchRoot d k args result)
+    | Key.star  => return (k, result)
+    /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
+    | Key.arrow => return (k, (← getMatchRoot d k args (← getMatchRoot d .other #[] result)))
+    | _         => return (k, (← getMatchRoot d k args result))
 
 /--
   Find values that match `e` in `d`.

tests/lean/run/1549.lean

@@ -0,0 +1,18 @@
+theorem not_mem_nil (a : Nat) : ¬ a ∈ [] := fun x => nomatch x
+
+theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) :
+  (∀ h' : p, q h') ↔ True := sorry
+
+example (R : Nat → Prop) : (∀ (a' : Nat), a' ∈ [] → R a') := by
+  simp only [forall_prop_of_false (not_mem_nil _)]
+  exact fun _ => True.intro
+
+
+def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
+theorem iff_of_true (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩
+theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h ⟨⟩
+
+example {P : Prop} : ∀ (x : Nat) (_ : x ∈ []), P :=
+by
+  simp only [forall_prop_of_false (not_mem_nil _)]
+  exact fun _ => True.intro