for x being set
for f being FinSequence st f just_once_values x holds
Rev (f -| x) = (Rev f) |-- x