push_neg at hC
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬((𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2))
⊢ False
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False