rcases this with ⟨Z, con, ss, hZ⟩
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
this : ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
case intro.intro.intro
α : 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
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z