induction p using rec' generalizing t with
| himp p q ihp ihq =>
  constructor;
  . 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;
  . simp [Satisfies.imp_def];
    intro h t' htt' hp;
    replace hp := ihp.mp hp;
    have hpq := htt' h;
    apply ihq.mpr;
    apply t'.not_mem₂_iff_mem₁.mp;
    exact not_mem₂
      (by simp_all)
      (show 𝓓 ⊢! [p, p ⟶ q].conj' ⟶ q by
        simp;
        apply andImplyIffImplyImply'!.mpr;
        apply deduct'!;
        apply deduct!;
        exact by_axm! ⨀ (by_axm! (p := p));
      );
| _ => simp [Satisfies.iff_models, Satisfies, *];
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ↔ p ∈ t.tableau.1
no goals