proposition: Lemma list_size_fold : forall (A : Type) (size : A -> nat) l, (fix size_list (l0 : list A) : nat := match l0 with | nil => 0 | t :: lt => size t + size_list lt end) l = list_size size l.
proof: Proof. intros A size l; induction l; trivial. simpl; rewrite IHl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)