I’m very happy with the funelim tactic except for the new variable names it introduces. I would like to control the names chosen (as with the induction tactic). Currently I use for instance
funelim (dnf C D); rename C0 into C; try rename l into D; try clear Heq; try rename H into IH; try rename H0 into IH'.
to cover all of the (many) cases resulting from the defining equations of the function dnf. This is unsatisfactory since the script will break if Equations changes its naming policy. As quick fix the inductive hypotheses could be named IHn, and the names given in the patterns of the defining equations could be preserved. Also the Heq’s could be eliminated by default. This would get rid of all clears and renames in the example above.