exact (Gentzen.inconsistent_of_provable_and_refutable b₁ b₂).not_con consis
case intro.intro
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
b₁ : T ⊢ σ
b₂ : T ⊢ ~σ
⊢ False
no goals