simp only [eval_conj, eval_neg]
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ (conj φ (neg φ)) ≤ eval τ fls
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ (eval τ φ && !eval τ φ) ≤ eval τ fls