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