Added constructs for dealing with pairs:
- The function pair : t1 -> t2 -> t1*t2  makes a pair
- The function proj1 : t1*t2 -> t1   gets the first projection
- The function proj2 : t1*t2 -> t2   gets the second projection

Propagated the changes to mconbase2.v, and modified the proofs such that
they still work (note some of the section comments may be incorrect
now).