proposition: Lemma permut_app2 : forall (A : Type) (R : relation A), Equivalence R -> forall l l1 l2, permut0 R l1 l2 <-> permut0 R (l1 ++ l) (l2 ++ l).
proof: Proof. intros A R E l l1 l2; split; intro P. induction l as [ | u l]. do 2 rewrite <- app_nil_end; trivial. apply permut_strong; trivial. reflexivity. induction l as [ | u l]. do 2 rewrite <- app_nil_end in P; trivial. apply IHl. apply (@permut_add_inside A A R u u); trivial. intros a1 b1 a2 b2 _ _ _ _ a1_R_b1 a2_R_b1 a2_R_b2; transitivity b1; trivial. transitivity a2; trivial. symmetry; trivial. reflexivity. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)