proposition: Lemma list_size_app: forall (A : Type) (size : A -> nat) l1 l2, list_size size (l1 ++ l2) = list_size size l1 + list_size size l2.
proof: Proof. induction l1 as [ | a1 l1 ]; trivial. intros; simpl; rewrite IHl1; auto with arith. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)