proposition: Lemma permut0_refl : forall l, permut0 eq_A l l.
proof: Proof. intro l; apply permut_refl. intros a _; reflexivity. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)