[...]
the transaction Tx3 is special (this would need an extension of the scripting language). In order to use it, one needs to provide two *different* spendings of B0.
[...]
There is nothing stopping Tx3 from being broadcast and accepted by the network [...]
As he said it is a special TX. [...]
I feel like this is a grey area with the proposal. You cannot simply assume there exists a feasible extension to scripting which would allow the network to verify that a double spend occurred.
Also, what happens when the payer double-spends to another merchant using this proposal's mechanism? Who's Tx3 would be valid?