simp under binders

Stream: lean4

[David Renshaw]

In Lean 3, this example proof works:

@[simp] theorem not_mem_nil (a : nat) : ¬ (a ∈ ([] : list nat)) := id

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' ∈ ([]: list nat) → R a') :=
begin
  simp only [forall_prop_of_false (not_mem_nil _)],
  exact λ n , true.intro
end

However, after translation into Lean 4, the example proof fails at the simp only step:

@[simp] theorem not_mem_nil (a : Nat) : ¬ a ∈ [] := fun.

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 _)]
  -- (fails to simplify)

  sorry

Is there some way to make this work? Is Lean 4's simp missing some features that are present in Lean 3's simp?

[Leonardo de Moura]

Could you please create an issue on GitHub? Thanks.

[David Renshaw]

https://github.com/leanprover/lean4/issues/1549