assumption
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
this : f w₁ ⊧ p
hw₂ : f w ≺ f w₁
⊢ Satisfies M₂ (f w₁) p
no goals