pairwise implying R a b

Stream: Is there code for X?

[Yakov Pechersky]

Is there a shorthand lemma for something like?

lemma list.pairwise.mem_mem_ne_imp
{l : list α} {R : α → α → Prop} (h : pairwise R l) (symm : symmetric R) ⦃a : α⦄ (ha : a ∈ l)
  ⦃b : α⦄ (hb : b ∈ l) (hne : a ≠ b) : R a b

[Bhavik Mehta]

docs#list.forall_of_pairwise perhaps?

[Aaron Anderson]

docs#list.rel_of_pairwise_cons is as close as we get, I think