have : T *⊢[L]! ⊥ := hC₂ ⨀ hC₁
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
⊢ False
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : T *⊢[L]! p ∧ T *⊢[L]! ~p
hC₁ : T *⊢[L]! p
hC₂ : T *⊢[L]! ~p
this : T *⊢[L]! ⊥
⊢ False