Provable equality is a congruence on closed terms

Reflexivity proves $s=s$, so closure puts it in $H$. If $s=t$ belongs to $H$, symmetry proves $t=s$, which belongs to $H$. If $s=t,t=u$ belong, transitivity proves $s=u$, which belongs to $H$. These give precisely reflexivity, symmetry and transitivity of $\sim$.

If $s\sim t$ and $\alpha$ is a formula, the terms $s,t$ are free for any variable $x$ because they have no free variables. Equality substitution and MP give $H⊢\alpha [s\mathrm{/}x]\to \alpha [t\mathrm{/}x]$; symmetry gives the reverse implication. When the instances are sentences, closure and MP show their memberships in $H$ agree. If they retain other free variables, the same implication proofs remain valid without claiming that open formulas are members of $H$.

Let $s_i\sim t_i$ for $1\le i\le n$. Replace the tuple entries in order, applying step 2.1 at one placeholder variable absent from all the other displayed terms and formulas. Closed substituted terms cannot introduce or capture a variable. At every replacement the two closed instances have the same membership; transitivity of logical equivalence proves this for the full tuple. This applies to $R(s_1,\dots ,s_n)$ and to arbitrary closed formula instances. For $n=0$ no replacement is performed and the formula is identical.

For a function $f$, begin with the reflexive equation $f(\bar{s})=f(\bar{s})\in H$. Replace the entries in the right-hand occurrence alone in decreasing order $i=n,n-1,\dots ,1$, using the formula $f(\bar{s})=f(s_1,\dots ,s_{i-1},z,t_{i+1},\dots ,t_n)$. At this stage the entries to its right have already been replaced and the entries to its left have not. Step 2.1 gives each successive equality, ending with $f(\bar{s})=f(\bar{t})\in H$. Thus the function outputs are equivalent. A constant is its own fixed class; if there are no function or relation symbols, the equivalence relation proof still applies.