fact: Definition length A (l:list A) : nat := fold_right (fun x acc => 1+acc) 0 l.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)