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


Look at this file


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

Going home
Pierre Castéran