Support for subtrait matching in assume_specification

[parno]

Suppose I want to provide an ensures clause for str::contains, which operates on a Pattern. I can introduce the contains function and the Pattern trait to Verus like this.

    type ExternalTraitSpecificationFor: Pattern;
}

pub assume_specification <P: Pattern>[ std::primitive::str::contains ](
    s: &std::primitive::str,
    pat: P,
) -> (b: bool);```
Ideally, the postcondition of `contains` would be expressed in terms of some spec function of `P`, but we currently can't add spec functions to an existing trait.

To work around this, we could define a subtrait of `Pattern`, e.g.,
```trait PatternSpec : Pattern {
    spec fn is_contained_in(self: &Self, haystack: &str) -> bool;
}```
and then try to use that instead of `Pattern` in assume_specification:
```pub assume_specification <P: PatternSpec>[ std::primitive::str::contains ](
    s: &std::primitive::str,
    pat: P,
) -> (b: bool);```
but Verus currently expects an exact match.  If we relaxed this restriction to allow for subtrait matching, then this approach would work as a stopgap until we have the ability to attach spec functions to existing traits.