proposition: Lemma cardinal_Same_set {U} (A B : Ensemble U) x (H : Same_set _ A B) (H' : cardinal _ A x) : cardinal _ B x.
proof: Proof. destruct H' as [ls H']. exists ls. destruct_head and; split; auto. eapply EnsembleListEquivalence_Same_set; eassumption. Qed.
imports: Coq.Lists.List Coq.Sets.Ensembles Fiat.Common Fiat.Common.List.PermutationFacts Fiat.Common.Ensembles.EnsembleListEquivalence