One-pass substitution

[EnguerrandPrebet]

Update substitution to be one-pass by using a taboo set as a new parameter.
Apart from updating the substitution and the proofs accordingly, the main additions are:

• a custom computation of the bound variables after substitution substBoundVars which is proved correct Program.substBoundVars_applySubst_boundVars
• how reducing the taboo set leads to the same substitution (uniqueness is derived as a corollary)