no goals
α : Type u_1
β : Type ?u.4602
R S T : α → α → Prop
a : α
l✝ l : List α
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ a ∈ l → b ∈ l → R a b)
simp (config := { contextual := true }) only [forall_prop_of_true, iff_self_iff,
forall₂_true_iff]