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

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ⊓ φ₂ ↔ τ ⊨ φ₁ ∧ τ ⊨ φ₂
Tactic:
simp [sEntails, satisfies, Inf.inf]
State after:
no goals