Dependent pattern match on pairs doesn't work; need to use nested pattern-match instead

The following snippet doesn't work:

```
module JH

type vec (a: Type): nat -> Type =
| Nil: vec a 0
| Cons: hd:a -> n:nat -> tl:vec a n -> vec a (n + 1)

val map2:
n:nat ->
f:('a -> 'b -> Tot 'c) ->
l1:vec 'a n ->
l2:vec 'b n ->
Tot (vec 'c n)
let rec map2 n f l1 l2 =
match l1, l2 with
| Cons hd1 n1 tl1, Cons hd2 n2 tl2 ->
Cons (f hd1 hd2) n1 (map2 n1 f tl1 tl2)
| Nil, Nil ->
Nil
```

The following snippet does:

```
module JH

type vec (a: Type): nat -> Type =
| Nil: vec a 0
| Cons: hd:a -> n:nat -> tl:vec a n -> vec a (n + 1)

val map2:
n:nat ->
f:('a -> 'b -> Tot 'c) ->
l1:vec 'a n ->
l2:vec 'b n ->
Tot (vec 'c n)
let rec map2 n f l1 l2 =
match l1 with
| Cons hd1 n1 tl1 ->
begin match l2 with
| Cons hd2 n2 tl2 ->
Cons (f hd1 hd2) n2 (map2 n2 f tl1 tl2)
end
| Nil ->
begin match l2 with
| Nil ->
Nil
end
```

I made a quick note of it at https://github.com/FStarLang/FStar/wiki/Early-stumbling-blocks%2C-FAQ#error-pairs because I remember a discussion we had a while ago while I was playing with union-find, and @nikswamy was telling me that nested pattern-matches were better.

If I hallucinated / this is no longer the case / this bug can be fixed easily, then I'll make sure I remove the note in the wiki.

Thanks,

Jonathan