simp
α : 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
⊢ T ⊆ insert (~p) T
no goals