Does that work for X being the real numbers?
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).
But Haskell's quickCheck doesn't seem to find a problem.
λ quickCheck @(Float -> Bool) $ \x -> 2 * x == x + x
+++ OK, passed 100 tests.
λ quickCheck @(Double -> Bool) $ \x -> 2 * x == x + x
+++ OK, passed 100 tests.
λ quickCheck @(Double -> _) $ \a b c ->
(a + b) + c == a + (b + c)
*** Failed! Falsifiable (after 6 tests and 4 shrinks):
20.0
3.5741489348898856
2.894651135185324From the perspective of an Agda-phobe: The "2*x vs x+x" example could be a case of a general question about arithmetic expressions, or it could even just be about multiplication and addition. Since multiplication of integers can be defined as repeated addition, proving equality in that particular case for any numeric type just takes a rewrite of both sides in terms of addition only. If the coefficient ("2") was not a natural number, things would be a little more complicated (as other comments mention, you'd have to introduce some way of getting things into a canonical form). I guess that would be an "intensional" approach.
The best story I have about extensional definitions is a true one. At a class on bike repair, somebody asked what a fixed-wheel bike was. The instructor started to give an extensional definition: "It's like... a unicycle." Presumably he could have followed this with other examples such as a Penny Farthing -- but the audience seemed satisfied. It would obviously have been more helpful to give an intensional definition ("no gears".)
It would work with Coq's real number type but as the same properties wouldn't always hold with hardware float types, you may have trouble running the program if you extracted it to e.g. Haskell (as your example shows)?
The QuickCheck tests would pass if you allowed a small difference between them to account for floating point inaccuracies I imagine.