Update the proof of the substituion lemma of breduce. The lemma seems unprovable because of the dependency of nominal constants in the context