obtain ⟨T, hp₁, hp₂, hp⟩ := by simpa [Disjoint] using h;
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
⊢ False
case intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp : ¬T ⊆ ∅
⊢ False