Added tactic for case analysis.
Also, induction now work on expressions instead of simply names.