method SetOfSeq(a: seq<string>) returns (r: set<string>)
  // TODO

method SequenceInclusionWithSet(a: seq<string>, b: set<string>) returns (r: bool)
  // TODO

method SequenceInclusion(a: seq<string>, b: seq<string>) returns (r: bool)
  ensures r == (forall x :: x in a ==> x in b)
{
  var b' := SetOfSeq(b);
  var t := SequenceInclusionWithSet(a, b');
  return t; // (1) Write specs above so this method verifies.
            //     Just write the spec, no { ... } method body.
}

method SequenceInclusion_alt(a: seq<string>, b: seq<string>) returns (r: bool)
  ensures r == (forall x :: x in a ==> x in b)
{
  var a' := SetOfSeq(a);
  var b' := SetOfSeq(b);
  return true; // (2) Lean in to set operations and implement a different way
}