induction p using Semiformula.rec' <;>
  simp [*, Language.Hom.rel_add₁, Semiformula.eval_rel,
    Semiformula.lMap_rel, Semiformula.eval_nrel, Semiformula.lMap_nrel]
L₁ : Language
L₂ : Language
M : Type u_1
str₁ : Structure L₁ M
str₂ : Structure L₂ M
μ : Type u_2
n : ℕ
p : Semiformula L₁ μ n
e : Fin n → M
ε : μ → M
⊢ (Semiformula.Eval (add L₁ L₂ M) e ε) ((Semiformula.lMap (Language.Hom.add₁ L₁ L₂)) p) ↔ (Semiformula.Eval str₁ e ε) p
no goals