have : v ⊧* T := Semantics.RealizeSet.of_subset hv (by simp)
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
⊢ False
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this : v ⊧* T
⊢ False