contrapose
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
⊢ T ⊨[Valuation α] p → T ⊢! p
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
⊢ ¬T ⊢! p → ¬T ⊨[Valuation α] p