Some proofs in predicate calculus

Please edit this file and remove all calls to the auto tactic.