Theorem: LO.Gentzen.inconsistent_iff_nonempty (Logic/Logic/Calculus.lean)

State before:
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.Inconsistent 𝓣 ↔ Nonempty (𝓣 ⊢' [])
Tactic:
simp [←System.not_consistent_iff_inconsistent, consistent_iff_isEmpty]
State after:
no goals