The first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.