constructor
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) ↔ X⊨[φ]
case mp
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) → X⊨[φ]

case mpr
X : List Formula
φ : Formula
⊢ X⊨[φ] → ¬satisfiable (X ∪ [~φ])