case right =>
  intro hom h
  apply Hom.ext
  funext c
  induction c
  case a.h.var => simp [algebraHom, algebraHomImpl, h _]
  case a.h.app σ cs hi =>
    simp [algebraHom, algebraHomImpl]
    have h := hom.property σ cs
    simp [Term.algebra] at h
    simp [h]
    congr
    funext i
    exact hi i
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (y : Hom (Term.algebra Δ H) target),
    (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = Term.algebraHom target f
no goals