Theorem: LO.FirstOrder.Structure.HomClass.val_term (Logic/FirstOrder/Basic/Semantics/Elementary.lean)

State before:
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : HomClass F L M₁ M₂
φ : F
n : ℕ
μ : Type u_6
e : Fin n → M₁
ε : μ → M₁
t : Semiterm L μ n
⊢ φ (Semiterm.val s₁ e ε t) = Semiterm.val s₂ (⇑φ ∘ e) (⇑φ ∘ ε) t
Tactic:
induction t <;> simp [*, Semiterm.val_func, HomClass.func, Function.comp]
State after:
no goals