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