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