rcases hu with ⟨ssu, hu⟩
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
hu : ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
⊢ T ⊢! σ