no goals
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b
induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]