= Intro

n = n è vera per qualsiasi constante n e si può inferire in qualunque punto della prova

= Elim

• se nelle premesse o nei passaggi precedenti ho n = m, allora posso sostituire m al posto di qualunque occorrrenza di n in una proposizione P(n) già dimostrata, inferendo una nuova proposizione P(m)