proposition: Theorem permut_refl : forall (l : list A), permut 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)