Equivalence of two lambda expressions for NOT

I've seen two different lambda expressions for the logical NOT function.

One of them just applies its parameter to constants true and false internally in a reverse order:

$NOT \;\;=\;\; \lambda x.\; x \; \mbox{false}\; \mbox{true} \;\;=\;\; \lambda x. \; x \; (\lambda t.\lambda f.f) \; (\lambda t. \lambda f. t ) $

and the other one which captures two more parameters instead of passing them to the returned function externally, and applies $x$ to them in reverse order too:

$NOT \;\;=\;\; \lambda x. \; \lambda t.\lambda f.xft$

of which the other one seems a bit simpler (and it is also simpler when encoded in binary).

So my question is this:

Is there any transformation which could get me from one of these representations to the other?

I see they are equivalent "extensionally", that is, both produce the same results. But I'd like to "prove" it somehow by algebraic transformations, such as those for alpha, beta and eta conversions. Unfortunately, none of these can help me in this case: Alpha is just for renaming. Beta works only for function calls, but we don't have any function call here which could be reduced, since $x$ is free in the function body (not the whole expression, though) in all these expressions until we actually call NOT on something. The most close one seems to be the eta, which is related to extensional equivalence and forwarding parameters, but when the parameters are being reversed, it's not a simple forwarding anymore and eta doesn't seem to apply here.

Is there any more conversion rule I'm missing?

(Well, I guess they won't just skip two Greek letters from no particular reason, wouldn't they?)

P.S.: This question is actually a model one, since there are many other definitions for other functions which have several different forms which seem to be extensionally equivalent, but completely different with regard to the known reduction rules. I've chosen the simplest example of this problem.

Edit:

To better clarify what I'd like to know,

In order to prove the two NOT forms are not generally equivalent, all you have to do is find a term that when each is applied, returns a different result such as:

$NOT1 \; \lambda x.\; x \; \;\;=\;\; (\lambda x. \; x \; (\lambda t.\lambda f.f) \; (\lambda t. \lambda f. t )) \; \lambda x.\; x \;\; =\;\; \lambda x. \; x \; $

$NOT2 \; \lambda x.\; x \; \;\;=\;\; (\lambda x.\lambda t.\lambda f.xft) \; \lambda x.\; x\;\; =\;\; \lambda t.\lambda f. ft \; $

StackExchange Computer Science Q#14372, answer score: 3