feat(frontends/lean): add 'record' as an alias for 'structure' command
fix(frontends/lean/structure_cmd): error parsing structure without parameters followed by ': Type'
fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified
fix(frontends/lean/structure_cmd): bad test output
test(tests/lean/run): add structure command test
feat(frontends/lean): add 'print fields' command
feat(frontends/lean/structure_cmd): allow inheritance from two identical structures, closes #296
feat(library/hott) add theorem: if f is an equivalence, so is ap f
chore(library/hott) cleaned up the proof a bit
chore(library/hott) fixed the copyright in equiv_precomp.lean
fix(library/hott) rename IsEquiv.ap to IsEquiv.ap_closed to avoid name clashes
refactor(library/logic): cleanup some of the proofs in cast.lean, remove piext axiom

Remark: the main motivation for piext was Lean 0.1 simplifier.
We are using a different approach in Lean 0.2.
The axiom is not needed anymore.
It is also not used in any part of the standard library
fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.

Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).

This bug would confuse users and make them believe they define something
different.
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