case left =>
  intro ⟨v, hv⟩
  cases v
  case app => contradiction
  case var => simp [algebraHom, algebraHomImpl]
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (c : { a // Vars Δ H a }), f c = Hom.hom (Term.algebraHom target f) c.val
no goals