Theorem: LO.Gentzen.consistent_insert_iff_not_refutable (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
p : F
⊢ System.Consistent (cons p 𝓣) ↔ 𝓣 ⊬! ~p
Tactic:
simp [System.Unprovable, refutable_iff_inconsistent, System.not_inconsistent_iff_consistent]
State after:
no goals