prover [this]
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ maximalConsistentTheory consisT ⊢! q
no goals