Proof.Induction
genInduction