Add notations for monadic bind on products.
Improve [decompose_elem_of] tactic.
Change the definition of "is_Some" to use an existential.

Conflicts:
	memory_values.v
	pointers.v
	references.v
	types.v
Add "as ident(H)" to the "case_bool_decide" tactic.
Misc updates to the prelude.
Type classes for finite and countable types.
Add [reshape] function on lists.
Misc prelude changes.
Finite maps and sets using ordered association lists.

This commit includes the following changes:
* More theorems about pre-, partial and total orders.
* Define the lexicographic order on various commonly used data types.
* Mergesort and its correctness proof.
* Implement finite maps and sets using ordered association lists.

Conflicts:
	base.v
	pointers.v
	references.v
	types.v
More efficient conversion of pmap to association lists.
Prove better correspondence between Permutation and contains.
Make arguments of proj1_sig maximally implicit.
More properties about the rationals Qc.
Two basic De Morgan like laws for decidable propositions.
Use wf_projected instead of well_founded_lt_compat
Prove decidability of quantification over finite types.
Define lexicographical orders directly as a strict order.
Some theorems about zip and zip_with.