destruct evidence

Stream: new members

[Simon]

If I have a value of an inductive type in the context, which tactic do I use to extract the information provided when constructing the value? I am looking for something like inversion in Coq.

[Matt Diamond]

maybe tactic#injection?

[Reid Barton]

cases, induction, induction'

[Pedro Sánchez Terraf]

From recent experience: You need to import tactic.induction for induction'.