have : ¬v ⊧ p := by simpa using hv.realize (Set.mem_insert (~p) T)
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
this : v ⊧ p
⊢ 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
this✝ : v ⊧ p
this : ¬v ⊧ p
⊢ False