Use inductions instead of destructs in uu0

1. Notations such as paths_rect etc. are added for the eliminators of the inductive types that are used in
Foundations.

2. All "destruct"'s in uu0.v are replaced by "induction"'s. In several  places this required adding explicit 
names for the variables introduced by the "induction" tactic.