# Some proofs in predicate calculus

Consider the following declarations :
Section A_declared.
Variables (A : Set )
(P Q : A->Prop)
(R : A->A->Prop).

Prove the following theorems:
(forall a b:A, R a b) -> forall a b:A, R b a
(forall a:A, P a -> Q a) -> (forall a:A, P a) -> forall a:A, Q a
(forall a b:A, R a b) -> forall a:A, R a a

## Solution

Look at this file
### Note

Each of these proofs can be replaced by a simple call to `auto`.

Going home

Pierre Castéran