simpa using hZ U conU ssU
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
U : Theory α
conU : Consistent U
ssU : Z ⊆ U
⊢ U = Z
no goals