for D being non empty set
for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f -: p) = (Rev f) :- p