Theorem: LeanSAT.Model.PropFun.conj_neg_entails_fls (LeanSAT/Model/PropFun.lean)

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

State before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ (eval τ φ && !eval τ φ) ≤ eval τ fls
Tactic:
exact BooleanAlgebra.inf_compl_le_bot (eval τ φ)
State after:
no goals