intro h
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
⊢ hom₁.hom = hom₂.hom → hom₁ = hom₂
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
h : hom₁.hom = hom₂.hom
⊢ hom₁ = hom₂