Theorem: LeanSAT.Model.PropForm.satisfies_disj (LeanSAT/Model/PropForm.lean)

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ disj φ₁ φ₂ ↔ τ ⊨ φ₁ ∨ τ ⊨ φ₂
Tactic:
simp [sEntails, satisfies]
State after:
no goals