for f, g being FinSequence
for n, m being Nat st m >= n & g is_substring_of f,m holds
g is_substring_of f,n