no goals
α : Type u_1
β : Type ?u.9008
R S T : α → α → Prop
a✝ : α
l : List α
a b : α
⊢ Pairwise R [a, b] ↔ R a b
simp only [pairwise_cons, mem_singleton, forall_eq, forall_prop_of_false (not_mem_nil _),
  forall_true_iff, Pairwise.nil, and_true_iff]