simp_all
α : 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
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ∀ {w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.World} {a : α},
    { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Valuation w a ↔
      { Frame := F₂, Valuation := V₂ }.Valuation (f w) a
no goals