have := consistent_either consistent p
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
this : (𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)