proposition: Lemma list_size_size_eq : forall (A : Type) (size1 : A -> nat) (size2 : A -> nat) l, (forall a, In a l -> size1 a = size2 a) -> list_size size1 l = list_size size2 l.
proof: Proof. intros A size1 size2 l; induction l as [ | a l]; simpl; trivial. intros size1_eq_size2. rewrite (size1_eq_size2 a (or_introl _ (eq_refl _))). apply (f_equal (fun n => size2 a + n)); apply IHl; intros; apply size1_eq_size2; right; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)