`FStar.List.Tot.Properties.append_mem` is missing SMTPat

Hello!

I just found this very helpful property has its `SMTPat` commented out:

https://github.com/fstarlang/FStar/blob/master/ulib/FStar.List.Tot.Properties.fst#L191-L199

```fstar
val append_mem: #t:eqtype -> l1:list t
-> l2:list t
-> a:t
-> Lemma (requires True)
(ensures (mem a (l1@l2) = (mem a l1 || mem a l2)))
(* [SMTPat (mem a (l1@l2))] *)
let rec append_mem #t l1 l2 a = match l1 with
| [] -> ()
| hd::tl -> append_mem tl l2 a
```

For want of this pattern, we don't enjoy automated proof for properties such as

```fstar
let state_concat_has_both (vs vs': list vars) (s:state{state_has s (vs @ vs')})
: Lemma (state_has s vs /\ state_has s vs')
= ()
```

In general, it seems like a useful prop to have in the theory of lists. I assume this was commented out for a reason, but the `git blame` doesn't turn up anything obvious for me.

Would it be feasible to uncomment this? If not, perhaps a comment can be added explaining why it is omitted.

I'd be pleased to contribute either change, in case that is helpful.

Thanks for the amazing software!