A little doubt on the usage of the $(=\; elim)$ rule? I'm reading Language, Proof and Logic. I'm trying to understand this proof:



"= Intro" and "= Elim" are:



I understand the use of "= Intro" in the proof, but how exactly are we using "= Elim"? What is $p(n)$? I suspect $p(n) := [n=b]$. So we have in the fourth line:

*

*$p(b)$ which means $b=b$

*$b=a$

*$p(a)$ which means $a=b$
Is that it?
 A: Almost!  The $P(n)$ is a formula that has some number of instances of the variable-free term $n$, and the $P(m)$ is the formula that is the result of replacing zero or more of those $n$'s with $m$'s given that $n = m$
So ... the '$n=m$' claim corresponds to the $b = a$ claim on line 2, meaning that the '$n$' is $b$, and the '$m$' is $a$. The '$P(n)$' is $b = b$ on line 3, and the $P(m)$ is $a=b$ on line 4.
So yes, you correctly identified that the $b=a$ claim was the 'substitution' claim that you applied to the claim $b=b$ ... but it is not quite true that the '$P(n)$' claim is $n = b$.... it is simply $b=b$.
However, I think you were trying to think about it this way:
Let the formula $P(x)$ be the expression $x = b$
Then $P(b)$ is the result of taking formula $P(x)$, and instantiating the free variable $x$ with constant $b$.
So, $P(b)$ is $b = b$
Likewise, $P(a)$ is the result of taking formula $P(x)$, and instantiating the free variable $x$ with constant $a$.
So, $P(a)$ is $ a = b$
Identifying a formula $P(x)$ of which both the 'before' expression $P(n)$  and the 'after' expression $P(m)$ are instances (or in our case $P(a)$ and $P(b)$) is indeed a helpful way to think about $= Elim$. It may also make it a little more clear as to why you don't have to replace all occurrences of some constant in an expression with some other constant.
That is, had we defined $P(x)$ as $x = x$, then $P(b)$ would still have been $b = b$, but $P(a)$ would then have been $a = a$.  And if $P(x)$ would have been $b = x$, then $P(a)$ would have been $b = a$.
Perversely, we could even have defined $P(x)$ as $b = b$. Then $P(a)$ would still have been $b = b$. So, if you infer $b = b$ from $b = b$ and $b = a$ using $= Elim$ in the proof-checker software, it should still check out. Try it!
A: Equality elimination is a rule of substitution:  When $n=m$ is given then we may substitute any (some or all) occurrences of $n$, in a statement, for $m$ .
When $P(n)$ is a statement containing some occurrences of $n$, then $P(m)$ is that statement with those occurrences replaced with $m$, and so when we have the equality $n=m$ we may 'eliminate' this to say: $$\begin{array}{l}P(n)\\n=m\\\hline P(m)\end{array}$$
So your proof is using equality elimination to make the inferences that:
$$\begin{array}{l}3.~b=b\\2.~b=a\\\hline4.~a=b\hspace{4ex}{=}\textsf{E 3,2}\end{array}\qquad\begin{array}{l}1.~\operatorname{SameRow}(a,a)\\4.~a=b\\\hline5.~\operatorname{SameRow}(b,a)\hspace{2ex}{=}\textsf{E 1,4}\end{array}$$
Where the equality being 'eliminated' is the second line referenced in the rule, and has the form [original] = [substitute].
The first inference is a common subproof using equality introduction to 'flip' an equality around so we have the required order for the second inference.

So we put this together with the equality introduction to claim:
$$\begin{array}{|l}1.~\operatorname{SameRow}(a,a)\\2.~b=a\\\hline3.~b=b\hspace{12ex}{=}\textsf{I}~\\4.~a=b\hspace{12ex}{=}\textsf{E 3,2 }\\5.~\operatorname{SameRow}(b,a)\hspace{2ex}{=}\textsf{E 1,4}\end{array}$$

