So I have this
and I understand all except the Step 8.
$$ \neg r\equiv q, \neg r\lor q\vdash q\lor q$$
I don't know how can I use Leibniz rule of inference to get to that.
Definition of Leibniz Rule is given as:
$$X=Y, E[z := X] ⊢ E[z := Y] $$
If someone can explain that to me It would be great!
I've never heard of the 'Leibniz rule' in the context of propositional logic, but given Leibniz' Law that states that two objects are identical if and only if they share the exact same set of properties, and also looking at the use of the 'Leibniz rule' in the provided proof, I am $99$% sure the Leibniz rule says that if you have a biconditional $\phi \equiv \psi$, and you have some other statement that contains $\phi$, then in that latter statement you can infer any statement that has any of those $\phi$'s replaced ('substituted') with $\psi$'s.
So, in your case: we have the biconditional $\neg r \equiv q$, and we also have statement $\neg r \lor q$. That means that we can 'substitute' the $\neg r$ in the latter statement with $q$, and that results in $q \lor q$
Step 10 is a very special case of the Leibniz rule, where the statement you have ($q$) is in fact just one side of the biconditional $\neg r \equiv q$. But, you can see that if you then substitute $\neg r$ for $q$ in the statement $q$, you do indeed end up with $\neg r$