proposition: Lemma permut_app2 : forall l l1 l2, permut l1 l2 <-> permut (l1 ++ l) (l2 ++ l).
proof: Proof. intros l l1 l2; apply permut_app2. apply EDS.EQA. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)