rintro ⟨b₁⟩ ⟨b₂⟩
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
⊢ T ⊢! σ → ¬T ⊢! ~σ
case intro.intro
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
b₁ : T ⊢ σ
b₂ : T ⊢ ~σ
⊢ False