Replace fully axiomatic Seq with a model

[tchajed]

The following datatype should be adequate as a model for all of the sequence axioms:

#[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.