have := completeness ⟨[φ], [], none⟩
φ : Formula
⊢ consistent ([φ], [], none) ↔ satisfiable φ
φ : Formula
this : consistent ([φ], [], none) ↔ satisfiable ([φ], [], none)
⊢ consistent ([φ], [], none) ↔ satisfiable φ