induction p using Formula.rec' generalizing w with
| hatom p =>
  constructor;
  . apply hMor.atomic |>.mp;
  . apply hMor.atomic |>.mpr
| hbox p ih =>
  simp;
  constructor;
  . intro h w₂ hw₂;
    obtain ⟨w₁, ⟨hww₁, e⟩⟩ := hMor.back hw₂;
    have := ih.mp $ h w₁ hww₁;
    subst e;
    assumption;
  . intro h w' hww';
    exact ih.mpr $ h (f w') $ hMor.forth hww';
| _ => simp_all;
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
w : M₁.World
⊢ w ⊧ p ↔ f w ⊧ p
no goals