Qualifiers on indices of inductive are not strictly checked

Both of the definitions below are accepted, but only the second one should work.
```fstar
module Bug

type test : int -> Type =
| Make :
i:int ->
test 23

let proj_0 #i (r : test i) : int = match r with | Make #i -> i
let proj_1 #i (r : test i) : int = match r with | Make i -> i
```

Start by reproducing the two F* definitions from the issue and compare how the inductive index qualifiers are checked in each match. Done means the definition using `Make #i` is rejected while the definition using `Make i` remains accepted.

Written by the indexing model from the issue text.