fact: Fixpoint take A (n:nat) (l:list A) : list A := match n with | 0 => nil | S n' => match l with | nil => nil | a::l' => a::(take n' l') end end.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)