I have inductively defined
Foo (m: nat) f defined alike
Inductive Foo (m: nat) f := | Foo0 : Bar f -> Foo 0 f | FooS : forall (m: nat), Baz (Foo m) f -> Foo m.+1 f
Then, I destructured it as follows.
(* I had a hypothesis (Hm: Foo m.+1 f) here *) case Eq: m'.+1 f / Hm=> //.
Now I got bunch of variables like
I heard this method of inversion gives me more control, so I did not expect this.
Why is this happening? Is there a way to assign names that I want?
I also cannot use these hypothesis, it says "identifier is reserved".
IIRC you can introduce them (and give names) after the =>. Usually ssreflect would let you leave them in the goal, but that'd be ill-typed here, since you're introducing Eq.
Thank you! I was confused because it gave a branch, so I needed to introduce variables for each branch.
Last updated: Feb 08 2023 at 08:02 UTC