generalizeTargets but customized for the
Given a metavariable
mvarId representing the
Ctx, h : I A j, D |- T
hs id, and the type
I A j is an inductive datatype where
A are parameters,
j the indices. Generate the goal
Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T
(j == j' -> h == h') is a "telescopic" equality.
j is sequence of terms, and
j' a sequence of free variables.
The result contains the fields
casesOn using the free variable
majorFVarId as the major premise (aka discriminant).
givenNames contains user-facing names for each alternative.