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.

Learning resources