congr
Δ : 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
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ Algebra.θ target σ (hom.hom ∘ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)
case e_a
Δ : 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
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ hom.hom ∘ cs = fun x => Term.algebraHomImpl target f (cs x)