Replace fully axiomatic Seq with a model

The following datatype should be adequate as a model for all of the sequence axioms:

```rs
#[verifier::accept_recursive_types(A)]
pub enum Seq<A> {
    Nil,
    Cons(A, Box<Seq<A>>),
}
```

We should use this as the model and prove the current set of axioms against it.