UniMath/UniMath — pull request #37 by vladimirias (2014-10-24 11:57:21+00:00)
Title: 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.