simp only [eval_conj, eval_disj]
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ (conj (disj φ₁ φ₂) (disj φ₁ φ₃)) ≤ eval x✝ (disj φ₁ (conj φ₂ φ₃))
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ ((eval x✝ φ₁ || eval x✝ φ₂) && (eval x✝ φ₁ || eval x✝ φ₃)) ≤ (eval x✝ φ₁ || eval x✝ φ₂ && eval x✝ φ₃)