proposition: Lemma EnsembleListEquivalence_Permutation U (A : Ensemble U) ls ls' (H : EnsembleListEquivalence A ls) (H' : EnsembleListEquivalence A ls') : Permutation ls ls'.
proof: Proof. revert A ls' H H'. induction ls; intros A ls' H H'. { destruct_head_hnf and; split_iff. destruct ls'; simpl in *; auto. specialize_all_ways. intuition. } { let H := fresh in let H' := fresh in let t := destruct_head_hnf and; split_iff; intuition in lazymatch goal with | [ |- Permutation (?a::?ls) ?ls' ] => assert (H : List.In a ls') by t; assert (H' : ~List.In a ls) by (intro; t; match goal with | [ H'' : NoDup (_::_) |- _ ] => solve [ inversion H''; subst; intuition ] end) end; hnf in H. destruct (Permutation_pull_to_front _ _ H0) as [ls'' H'']. symmetry in H''. etransitivity; [ | exact H'' ]. apply perm_skip. apply (IHls (Subtract _ A a)). { perm_t; specialize_all_ways; perm_t. } { pose proof (fun x => @Permutation_in _ _ _ x H''). symmetry in H''. pose proof (fun x => @Permutation_in _ _ _ x H''). let H := fresh in assert (H : NoDup (a::ls'')) by (eapply PermutationFacts.NoDup_Permutation_rewrite; try solve [ destruct_head_hnf and; eassumption ]); inversion H; subst; clear H. perm_t; specialize_all_ways; perm_t. } } Qed.
imports: Coq.Lists.List Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common Fiat.Common.List.PermutationFacts