Coq-Equations
Coq-Equations copied to clipboard
Generalize funelim to take into account parameters of polymorphic
functions which shouldn't be generalized blindly. In general the strategy for generalizing the arguments of the function for functional elimination seems suboptimal. It might try to generalize arguments that are dependent (appear elsewhere in the goal) resulting in ill-typed generalizations. We might need the proper second_order_abstraction procedure of unifall to find the most general typable generalization of the goal w.r.t the arguments of the function to solve this problem.