induction l₁ <;> induction l₂ <;> aesop
α : Type u_1
inst✝² : LogicalConnective α
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
l₁ l₂ : List α
⊢ f (l₁ ++ l₂).conj ↔ f (l₁.conj ⋏ l₂.conj)
no goals