When we discussed this solution we said that we should do best effort leaving. The real thing will be implemented in 2.3, when we really need hand off and stuff. Or do you have a suggestion of how to solve it?
Changing leader semantics for leaving is not correct, I think.
The only thing I can think of is to treat unreachable Leaving special, so that it is always handled as auto-down.
However, I don't see the big problem, unreachable (and downing) can always happen.