suffices Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T) by
  contrapose
  intro hp hs
  have : Semantics.Satisfiable (Valuation α) (insert (~p) T) :=
    this (consistent_insert_iff_not_refutable.mpr $ by simpa)
  rcases this with ⟨v, hv⟩
  have : v ⊧* T := Semantics.RealizeSet.of_subset hv (by simp)
  have : v ⊧ p := hs this
  have : ¬v ⊧ p := by simpa using hv.realize (Set.mem_insert (~p) T)
  contradiction
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ T ⊨[Valuation α] p → T ⊢! p
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)