Equality introduction rule
= Equality introduction rule
{title2=$\dfrac{}{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$.