Theorem: LO.FirstOrder.Semiformula.lMap_bind (Logic/FirstOrder/Basic/Syntax/Rew.lean)

State before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
ξ₂ : Type u_3
ξ₁ : Type u_4
b : Fin n₁ → Semiterm L₁ ξ₂ n₂
e : ξ₁ → Semiterm L₁ ξ₂ n₂
p : Semiformula L₁ ξ₁ n₁
⊢ (lMap Φ) ((Rew.bind b e).hom p) = (Rew.bind (Semiterm.lMap Φ ∘ b) (Semiterm.lMap Φ ∘ e)).hom ((lMap Φ) p)
Tactic:
induction p using rec' generalizing ξ₂ n₂ <;>
simp[*, Rew.rel, Rew.nrel, lMap_rel, lMap_nrel, Semiterm.lMap_bind, Rew.q_bind, Matrix.comp_vecCons', Semiterm.lMap_bShift, Function.comp]
State after:
no goals