my_induction : introducing variable when defining tactic || naming more convenient way

[sven--]

Tactic Notation "my_induction" tactic(target) :=
induction target; simpl; intros; inversion H0; subst; try assumption; try reflexivity.

1. takes H0 as a parameter
2. forces (induction target;) to generate hypotheses with some special name.
   (I cannot specify number of branches (induction target) will make, and the only way I know to give name in generated hypotheses is specifying it one by one, which cannot be done here generally.)

[jeehoonkang]

let H := fresh "H" in induction x as [|x y H]; [|inv H].