fact: Fixpoint list_size (A : Type) (size : A -> nat) (l : list A) {struct l} : nat := match l with | nil => 0 | h :: tl => size h + list_size size tl end.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)