fact: Fixpoint seg (l: list A) (from size : nat) {struct from} : list A := match from, l with | 0, _ => initialSeg l size | _, nil => nil | S n, hd::tl => seg tl n size end.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)