proposition: Lemma Permutation_in' : forall {A : Type} {l l' : list A} (x : A), Permutation l l' -> (List.In x l <-> List.In x l').
proof: Proof. split; intros; eapply Permutation_in; [ | | symmetry | ]; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.Structures.OrderedTypeEx