Using ssreflect, I fell in love with its style of actively managing binders into and from the goal. However, I had problems with searching for what I want from its documentation.
In particular, I cannot find the ssreflect tactic for the inversion tactic.
I understand that I can very well use inversion tactic.
Yet, it follows the traditional coq style in using binders, where I am having hard time specifying correct names per branch as it is 'hidden' from the multiple goal view.
Meanwhile, ssreflect tactics always discharge the binders into the goal, so I could bind names to those alike move.
For instance, by applying inversion on Forall2 R l m, I get
x0: A
y0: B
l0: list A
l': list B
H3: R x y
H5: Forall2 R l m
H0: x0 = x
H1: l0 = l
H2: y0 = y
H4: l' = m
which are the names I do not like, and tracking and specifying those would be painful as the bindings are hidden behind the second branch (first branch is merely l = m = []).
What can I use if I want to invert an inductive type, in ssreflect style? Can elim be used for some kind of inversion?