simpa using this
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : maximalConsistentTheory consisT ⊢! p
this : p ∈ theory (maximalConsistentTheory consisT)
⊢ p ∈ maximalConsistentTheory consisT
no goals