for p being FinSequence
for x being object holds
( p just_once_values x iff len (p - {x}) = (len p) - 1 )