proposition: Lemma permut0_sym : forall l1 l2, permut0 eq_A l1 l2 -> permut0 eq_A l2 l1.
proof: Proof. intros l1 l2 P; apply permut_sym; trivial. intros a b _ _ a_eq_b; symmetry; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)