proposition: Lemma permut_sym : forall (A : Type) (R : relation A) l1 l2, (forall a b, In a l1 -> In b l2 -> R a b -> R b a) -> permut0 R l1 l2 -> permut0 R l2 l1.
proof: Proof. intros A R l1; induction l1 as [ | a1 l1]; intros l2 sym_R P; inversion P as [ | a b l1' l2' l2'' a_R_b Q]; subst. apply Pnil. apply (permut_strong (R := R) b a1 l2' l2'' (@nil A) l1). apply sym_R; trivial; [left | apply in_or_app; right; left]; trivial. simpl; apply IHl1; trivial. intros; apply sym_R; trivial; [right | apply in_insert]; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)