push_neg at hC
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬((L)-Consistent insert p T ∨ (L)-Consistent insert (~p) T)
⊢ False
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
⊢ False