proposition: Lemma permut_size : forall (A B : Type) (R : A -> B -> Prop) size size' l1 l2, (forall a a', In a l1 -> In a' l2 -> R a a' -> size a = size' a') -> permut0 R l1 l2 -> list_size size l1 = list_size size' l2.
proof: Proof. intros A B R size size' l1; induction l1 as [ | a1 l1 ]; intros l2 E P; inversion P as [ | a b l1' l2' l2'' a_R_b P']; subst; trivial. rewrite list_size_app; simpl. rewrite (E a1 b); trivial. rewrite (IHl1 (l2' ++ l2'')); trivial. rewrite list_size_app; simpl. rewrite Nat.add_comm. rewrite <- Nat.add_assoc. apply (f_equal (fun n => list_size size' l2' + n)). apply Nat.add_comm. intros a a' a_in_la a_in_l'; apply E; trivial. right; trivial. apply in_insert; trivial. left; trivial. apply in_or_app; right; left; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)