. contrapose;
  simp_all;
  intro h;
  replace h := t.not_mem₁_iff_mem₂.mp h;
  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;
  obtain ⟨t', ⟨⟨_, _⟩, _⟩⟩ := by simpa [Set.insert_subset_iff] using lindenbaum this;
  existsi t';
  simp_all;
  apply t'.not_mem₁_iff_mem₂.mpr;
  assumption;
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ⟶ q → p ⟶ q ∈ t.tableau.1

case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q