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