Induction on nat working
Improvment on readability and usability of induction and eliminators.
Fixed reflection induction tactic
Readded solveAll
Merge pull request #713 from ahmadsalim/feature/inductiontactic

Added support for induction tactic (works only for nonparameterized types insofar, requires eliminator for type)