constructor
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) ↔ Satisfiable (X ∪ {φ})
case mp
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) → Satisfiable (X ∪ {φ})

case mpr
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {φ}) → Satisfiable (X ∪ {~~φ})