 Equality elimination rule

From $s=t$ and $A(s)$, infer $A(t)$ by capture-free substitution. Rewriting in the opposite direction first uses symmetry of equality.