Subsequence(E): trait
  includes Sequence(E)
  introduces subsequence: Seq[E], Seq[E] -> Bool
  asserts with e, e1, e2: E, s, s1, s2: Seq[E] 
    subsequence({}, s);
    ~ subsequence(s |- e,{});
    subsequence(s1 |- e1, s2 |- e2) <=> subsequence(s1 |- e1, s2) \/
					(subsequence(s1,s2) /\ e1 = e2)