For two sequences s and t, s subsequence t tests whether the list of values taken by s occurs in the same order in the list of values taken by t.
letting s be sequence(1,1)
letting t be sequence(2,1,3,1)
find a : bool such that a <-> s subsequence t $ true
See it demonstrated here.