Theorem: tautImp_iff_comboNotUnsat (Bml/Semantics.lean)

State before:
ϕ ψ : Formula
⊢ Tautology (ϕ↣ψ) ↔ ¬Satisfiable {ϕ, ~ψ}
Tactic:
unfold Tautology
State after:
ϕ ψ : Formula
⊢ (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) (ϕ↣ψ)) ↔ ¬Satisfiable {ϕ, ~ψ}

State before:
ϕ ψ : Formula
⊢ (∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) (ϕ↣ψ)) ↔ ¬Satisfiable {ϕ, ~ψ}
Tactic:
simp
State after:
no goals