have : (𝓓)-Consistent (insert p t.tableau.1, {q}) := by
  simp only [Tableau.ParametricConsistent];
  intro Γ Δ hΓ hΔ;
  replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
    intro r hr;
    have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
    have := by simpa using hΓ r hr₁;
    simp_all;
  by_contra hC;
  have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
    apply deduct'!;
    apply deduct!;
    have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
    have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
    exact disj_allsame'! (by simpa using hΔ) this;
  )
  have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
  contradiction;
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1