proposition: Lemma permut_refl : forall (A : Type) (R : relation A) l, (forall a, In a l -> R a a) -> permut0 R l l.
proof: Proof. intros A R l refl_R; induction l as [ | a l]. apply Pnil. apply (@Pcons _ _ R a a l nil l). apply refl_R; left; trivial. simpl; apply IHl; intros; apply refl_R; right; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)