exact satisfiable_of_consistent consis
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
consis : Consistent (insert (~p) T)
⊢ Semantics.Satisfiable (Valuation α) (insert (~p) T)
no goals