replace hp := ihp.mp hp
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
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : Satisfies (CanonicalModel 𝓓) t' p
⊢ Satisfies (CanonicalModel 𝓓) t' 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
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q