On: A proof of proof by infinite descent

[someplaceguy]

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