discreteGhost adds a new variable y that memorizes the present value of a term as y:=t. This technique can be helpful when that value later needs to be related to during the proof.
y
y:=t
Learning resources