proposition: Lemma list_permut_app_app : forall l1 l2, permut (l1 ++ l2) (l2 ++ l1).
proof: Proof. intros l1 l2; apply permut_swapp; apply permut_refl. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)