Theorem: tautImp_iff_comboNotUnsat (Pdl/Semantics.lean)

State before:
φ ψ : Formula
⊢ φ⊨ψ ↔ ¬satisfiable [φ, ~ψ]
Tactic:
simp [formCanSemImplyForm, semImpliesLists, satisfiable, evaluate]
State after:
no goals