. simp only [Satisfies.imp_def];
  intro h v hv hp;
  exact ihq.mpr $ h (by simpa [IntDPCounterexampleModel]) $ ihp.mp hp;
case himp.mpr
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p✝ q✝ : Formula α
M₁ M₂ : Model α
w₁ : M₁.World
w₂ : M₂.World
p q : Formula α
ihp : ∀ {w : M₁.World}, Satisfies M₁ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) p
ihq : ∀ {w : M₁.World}, Satisfies M₁ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) q
w : M₁.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) (p ⟶ q) → Satisfies M₁ w (p ⟶ q)
no goals