Theorem: notsatisfnotThenTaut (Bml/Semantics.lean)

State before:
⊢ ∀ (φ : Formula), ¬Satisfiable (~φ) → Tautology φ
Tactic:
intro phi
State after:
phi : Formula
⊢ ¬Satisfiable (~phi) → Tautology phi

State before:
phi : Formula
⊢ ¬Satisfiable (~phi) → Tautology phi
Tactic:
unfold Satisfiable
State after:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → Tautology phi

State before:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → Tautology phi
Tactic:
unfold Tautology
State after:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) phi

State before:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → ∀ (W : Type) (M : KripkeModel W) (w : W), Evaluate (M, w) phi
Tactic:
simp
State after:
no goals