proposition: Lemma in_permut_in : forall (A : Type) l1 l2, permut0 (@eq A) l1 l2 -> (forall a, In a l1 <-> In a l2).
proof: Proof. assert (H : forall (A : Type) l1 l2, permut0 (@eq A) l1 l2 -> forall a, In a l2 -> In a l1). intros A l1 l2 P a a_in_l2; destruct (In_split _ _ a_in_l2) as [l2' [l2'' H]]; subst. destruct (permut_inv_right_strong (R := @eq A) _ _ _ P) as [a' [l1' [l1'' [a_eq_a' [H _]]]]]; subst. apply in_or_app; right; left; trivial. intros A l1 l2 P a; split; apply H; trivial. apply permut_sym; trivial; intros; subst; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)