proposition: Lemma permut_app1 : forall (A : Type) (R : relation A), Equivalence R -> forall l l1 l2, permut0 R l1 l2 <-> permut0 R (l ++ l1) (l ++ l2).
proof: Proof. intros A R E l l1 l2; split; intro P. induction l as [ | u l]; trivial. simpl; apply (@Pcons _ _ R u u (l ++ l1) (@nil A) (l ++ l2)); trivial. reflexivity. induction l as [ | u l]; trivial. apply IHl. apply (@permut_cons_inside A A R u u (l ++ l1) (@nil _) (l ++ l2)); 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)