simp only [Semantics.realizeSet_iff]
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ F₁ ⊧* T → F₂ ⊧* T
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ (∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f) → ∀ ⦃f : Formula α⦄, f ∈ T → F₂ ⊧ f