for D being non empty finite set
for a being length_equal_card_of_set FinSequence of bool D holds len a <> 0