feat(kernel/inductive): relax conditions for an inductive datatype in Prop to be able to eliminate into Type

The new relaxed version allows us to define the "accessability"
proposition and have an eliminator into Type.

See justification in the new comments at inductive.cpp
fix(frontends/lean): improve error message, addresses issue #299
fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop
fix(tests/lean): avoid 'sorry' in expected output
feat(library/logic): add well-founded recursion

It also removes the old well-founded induction theorem based on
classical principles
refactor(library/logic/wf): minimize dependencies
feat(library/logic): import wf.lean in logic/default.lean

We will use well-founded recursion in the definitional package
feat(library/hott) add thm: to give a section of a fibration it suffices to provide it for the image of an equivalence
feat(library/hott) add calc environment for equivalences
chore(library/hott) clean up Equiv namespace
chore(library/hott) clean up file and add class inference
chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it
feat(library/hott) add univalence axiom
chore(library/hott) adapted univalence axiom to suit notation in book and def in Coq.
Added substitution lemma for equivalence calculations