seq_pidgeon[T: TYPE, (IMPORTING fslib) S: finite_set[T]]: THEORY BEGIN IMPORTING seq_def w: VAR finite_seq[(S)] seq_pigeon_lem: LEMMA (FORALL (i,j: below(l(w))): i /= j IMPLIES w(i) /= w(j)) IMPLIES l(w) <= card(S) seq_pigeon_hole: THEOREM l(w) > card(S) IMPLIES (EXISTS (i,j: below(l(w))): i /= j AND w(i) = w(j)) END seq_pidgeon