Added tactic for case analysis.

Also, induction now work on expressions instead of simply names.