proposition: Lemma permut_app : forall (A B : Type) (R : A -> B -> Prop) l1 l1' l2 l2', permut0 R l1 l2 -> permut0 R l1' l2' -> permut0 R (l1 ++ l1') (l2 ++ l2').
proof: Proof. intros A B R l1; induction l1 as [ | a1 l1]; intros l1' l2 l2' P P'. inversion_clear P; trivial. inversion P as [ | a b l1'' l2'' l2''' a_R_b Q]; subst. simpl; rewrite <- ass_app; simpl; apply Pcons; trivial. rewrite ass_app; apply IHl1; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)