induction c
case a.h
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
c : (Term.algebra Δ H).carrier
⊢ Hom.hom hom c = Hom.hom (Term.algebraHom target f) c
case a.h.var
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
h✝ : H
⊢ Hom.hom hom (var h✝) = Hom.hom (Term.algebraHom target f) (var h✝)

case a.h.app
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ✝ : Δ.alphabet
v✝ : Fin (RankedAlphabet.rank Δ σ✝) → Term Δ H
v_ih✝ : ∀ (a : Fin (RankedAlphabet.rank Δ σ✝)), Hom.hom hom (v✝ a) = Hom.hom (Term.algebraHom target f) (v✝ a)
⊢ Hom.hom hom (app σ✝ v✝) = Hom.hom (Term.algebraHom target f) (app σ✝ v✝)