non-confluence of simp on List cons with reverse

Stream: lean4

[Bhavik Mehta]

open List

example {α : Type} (a : α) (l : List α) (p : α → Prop) :
    (∀ b ∈ (a :: l).reverse, p b) := by
  simp only [reverse_cons, mem_append, mem_reverse, mem_cons, not_mem_nil, or_false]
  show ∀ b, b ∈ l ∨ b = a → p b
  sorry

example {α : Type} (a : α) (l : List α) (p : α → Prop) :
    (∀ b ∈ (a :: l).reverse, p b) := by
  simp only [mem_reverse, mem_cons, forall_eq_or_imp]
  show p a ∧ ∀ b ∈ l, p b
  sorry

Each of the lemmas in the simp calls are existing simp lemmas in core, but selecting different ones leads to different simp-normal goals. We could add forall_or_eq_imp too, but it seems like the sensible RHS for that would have the And the other way round

[Jovan Gerbscheid]

There's already non-confluence like this:

open List

example {α : Type} (a : α) (l k : List α) :
    a ∈ (k ++ l).reverse := by
  simp only [reverse_append, mem_append, mem_reverse]
  show a ∈ l ∨ a ∈ k
  sorry

example {α : Type} (a : α) (l k : List α) :
    a ∈ (k ++ l).reverse := by
  simp only [mem_reverse, mem_append]
  show a ∈ k ∨ a ∈ l
  sorry