α : Type u_1
β : Type ?u.10097
R S T : α → α → Prop
a✝ : α
l : List α
s : Symmetric R
a : α
l₁ l₂ : List α
⊢ (Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ l₁ ++ [a] → ∀ (b : α), b ∈ l₂ → R a_1 b) ↔
    Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ [a] ++ l₁ → ∀ (b : α), b ∈ l₂ → R a_1 b
α : Type u_1
β : Type ?u.10097
R S T : α → α → Prop
a✝ : α
l : List α
s : Symmetric R
a : α
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
no goals
α : Type u_1
β : Type ?u.10097
R S T : α → α → Prop
a✝ : α
l : List α
s : Symmetric R
a : α
l₁ l₂ : List α
⊢ (Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ l₁ ++ [a] → ∀ (b : α), b ∈ l₂ → R a_1 b) ↔
    Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ [a] ++ l₁ → ∀ (b : α), b ∈ l₂ → R a_1 b
simp only [mem_append, or_comm]