Replace lists by sequences in Ortac/QCheck-STM tests

[n-osborne]

Fixes #278

This should also help #277.

I didn't change the tests for the wrapper mode as using sequences would mean supporting models (see #224)

[jmid]

LGTM!

Will :: be a short-hand for Sequence.cons in the revised stdlib, that removes List?
Comparing tuples.add it helps readability, IMO:

- ensures h.contents = match tup with a, b -> (a, b) :: old h.contents
+ ensures h.contents = match tup with a, b -> Sequence.cons (a, b) (old h.contents)

[n-osborne]

Sadly, I'm not sure.
It is not yet decided whether we will continue to allow importing pure OCaml value in Gospel. If so, :: will be reserved for OCaml lists. Is not, an argument can be make that allowing :: for Gospel sequences can be confusing?
But I agree that the prefix cons is not ideal.

TBH, I'm also a bit sad that we lose pattern matching too.