Yes. When we see a universal quantifier (e.g. 'forall (x : X)...') it's tempting to think that we're talking about the thing being quantified over (i.e. 'X'), b

Yes. When we see a universal quantifier (e.g. 'forall (x : X)...') it's tempting to think that we're talking about the thing being quantified over (i.e. 'X'), but in fact what we're saying is that the quantified thing is irrelevant. In the case of something like `\x. 2 * x` and `\x. x + x`, we're saying "forget about what 'x' might be, because it's irrelevant; look, I'll show you that we can use semantics-preserving rewrite rules to turn one of these syntax trees into the other". The resulting theorems work for all 'x' precisely because the proof doesn't need to know or care what the value of 'x' is, since it's just shuffled around as a symbol (part of the syntax tree).