. simp only [Satisfies.imp_def];
  intro h X hWX hp;
  obtain ⟨x, hx, ex⟩ : ∃ x, w ≺ x ∧ (Sum.inr $ Sum.inr x) = X := by
    replace hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel _ X := hWX;
    simp [IntDPCounterexampleFrame] at hWX;
    split at hWX;
    all_goals simp_all;
  subst ex;
  exact ihq.mp $ h hx $ ihp.mpr hp;
case himp.mp
α : 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.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
⊢ Satisfies M₂ w (p ⟶ q) → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q)

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.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q) → Satisfies M₂ w (p ⟶ q)
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.inr w)) p
ihq : ∀ {w : M₂.World}, Satisfies M₂ w q ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) q
w : M₂.World
⊢ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) (p ⟶ q) → Satisfies M₂ w (p ⟶ q)