[jepler]

I thought the same might be true, and a theorem prover agrees with us: https://gist.github.com/jepler/eda8401d1b613c44376dc8148fcf9...