intro h w' hww'
case hbox.mpr
α : 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
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
case hbox.mpr
α : 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), f w ≺ w' → Satisfies M₂ w' p
w' : M₁.Frame.World
hww' : w ≺ w'
⊢ Satisfies M₁ w' p