Minor improvement ideas

[berpeti]

• Unify naming of substitution theorems (e.g., evar_open_not_occur and evar_quantify_fresh should be named the same way, while evar_quantify_fresh_no_occurrence should be named differently).
• Theorems should be formulated with any proof constraint i, so that we can apply them without manually rewriting the contraints.
• Delete evar_is_fresh_in and svar_is_fresh_in.