induction p using rec' generalizing w with
| himp p q ihp ihq =>
  constructor;
  . 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;
  . simp only [Satisfies.imp_def];
    intro h v hv hp;
    exact ihq.mpr $ h (by simpa [IntDPCounterexampleModel]) $ ihp.mp hp;
| _ => simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies];
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
w : M₂.World
w₁ : M₁.World
w₂ : M₂.World
⊢ Satisfies M₂ w p ↔ Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p
no goals