simp at h
case mk.mk
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom✝¹ : alg₁.carrier → alg₂.carrier
property✝¹ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝¹ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝¹ ∘ cs)
hom✝ : alg₁.carrier → alg₂.carrier
property✝ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝ ∘ cs)
h : { hom := hom✝¹, property := property✝¹ }.hom = { hom := hom✝, property := property✝ }.hom
⊢ { hom := hom✝¹, property := property✝¹ } = { hom := hom✝, property := property✝ }
case mk.mk
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom✝¹ : alg₁.carrier → alg₂.carrier
property✝¹ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝¹ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝¹ ∘ cs)
hom✝ : alg₁.carrier → alg₂.carrier
property✝ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝ ∘ cs)
h : hom✝¹ = hom✝
⊢ { hom := hom✝¹, property := property✝¹ } = { hom := hom✝, property := property✝ }