for F being disjoint_valued FinSequence
for n being Nat holds Union (F | n) misses F . (n + 1)