I currently have the following:

```
Inductive var {V : nat} :=
| free (name : name)
| bound (l : Fin.t V).
Definition openv a {V} (v : @var (S V)) : @var V :=
match v with
| free n => free (shift_name a n)
| bound l =>
match l in Fin.t (S V) with
| Fin.F1 => free a
| Fin.FS l => bound l
end
end.
```

where Fin.t is the finite set type from Vectors.Fin. However, I’d like to write `openv`

in a more nested manner like so:

```
Definition openv a {V} (v : @var (S V)) : @var V :=
match v with
| free n => free (shift_name a n)
| bound Fin.F1 => free a
| bound (Fin.FS l) => bound l
end.
```

However, Coq complains that `The term "l" has type "Fin.t n" while it is expected to have type "Fin.t V".`

, despite the target `v`

having type `@var (S V)`

. I’m guessing this is in part because `(S V)`

is an index of `Fin.t`

, not a parameter. This is why I have `in Fin.t (S V)`

in the nested match in the first snippet.

Is there a way to write this in the nested form, but perhaps with some type or `in`

annotations? Something like `| bound (Fin.FS l in Fin.t (S V)) => ...`

for instance. Or is the first snippet the idiomatic way to write this?