. 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));
    );
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
no goals