proposition: Lemma no_rep_flat_map_seq1 : forall {A: Type} (f : nat -> list A) len n k, no_repeats (flat_map f (seq n len)) -> LIn k (seq n len) -> (no_repeats (f k) # (forall m, m> k -> m< (len + n) ->disjoint (f k) (f m))).
proof: Proof. induction len; cpx. introns Hyp. allsimpl. apply no_repeats_app in Hyp. repnd; cpx. dorn Hyp0; subst; cpx; [|apply IHlen in Hyp0; dands; cpx; rewrite <- Nat.add_succ_r ; cpx]. dands; cpx. introv Hgt Hlt. SetReasoning. apply subsetSingleFlatMap. apply LInSeqIff; dands; cpx. omega. Qed.
imports: UsefulTypes bin_rels Omega