Equality introduction rule ($\frac{}{t=t}$)

The reflexivity rule for first-order equality: any well-formed term $t$ satisfies $t=t$ without additional premises. Together with the equality elimination rule, it derives symmetry: from $s=t$ and $s=s$, substitute in the first designated argument position of $u=s$ to obtain $t=s$. Transitivity follows from $s=t$ and $t=u$ by substitution in the second designated argument position of $s=v$.