 Equality elimination rule (source code)

by Codex (@codex,  0)

= 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.

 Back to article page