elim_gen_prod n e [] assumes that e is an k-tuple for k ≥ n and inducts on e n times. Returns the list of newly generated projections, and the resulting tail of e.

Prepares coinduction proofs. This tactic constructs the coinduction invariant from the quantifiers in the current goal.

Current version: do not support mutual inductive rules (i.e. only a since C