simp [System.Consistent, System.not_consistent_iff_inconsistent, System.inconsistent_iff_provable_bot]
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬System.Consistent 𝓣 → ¬IsEmpty (𝓣 ⊢' [])
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢! ⊥ → Nonempty (𝓣 ⊢' [])