simp_all
case hor
α : 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✝ q✝ : Formula α
a✝¹ : ∀ {w : M₁.World}, w ⊧ p✝ ↔ f w ⊧ p✝
a✝ : ∀ {w : M₁.World}, w ⊧ q✝ ↔ f w ⊧ q✝
w : M₁.World
⊢ w ⊧ p✝ ⋎ q✝ ↔ f w ⊧ p✝ ⋎ q✝
no goals