intro h v hv 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.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
⊢ (∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
      Sum.inr (Sum.inr w) ≺ w' →
        Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q) →
    ∀ {w' : M₂.Frame.World}, w ≺ w' → Satisfies M₂ w' p → Satisfies M₂ w' 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
h :
  ∀ {w' : Unit ⊕ M₁.Frame.World ⊕ M₂.Frame.World},
    Sum.inr (Sum.inr w) ≺ w' →
      Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' p → Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) w' q
v : M₂.Frame.World
hv : w ≺ v
hp : Satisfies M₂ v p
⊢ Satisfies M₂ v q