tactic.cases_core

Stream: new members

[Kenny Lau]

What is the output of tactic.cases_core?

[Mario Carneiro]

/-- Apply `cases_on` recursor, names for the new hypotheses are retrieved from `ns`.
   `h` must be a local constant. It returns for each new goal the name of the constructor, a list of new hypotheses, and a list of
   substitutions for hypotheses depending on `h`. The number of new goals may be smaller than the
   number of constructors. Some goals may be discarded when the indices to not match.
   See `induction` for information on the list of substitutions.

   The `cases` tactic is implemented using this one, and it relaxes the restriction of `h`. -/

[Kenny Lau]

I don't really understand a list of substitutions for hypotheses and the fact that sometimes I get duplicates in that particular list