proposition: Lemma cardinal_unique {U} (A : Ensemble U) x y (H : cardinal _ A x) (H' : cardinal _ A y) : x = y.
proof: Proof. destruct_head_hnf ex. destruct_head and. subst. apply Permutation_length. eapply EnsembleListEquivalence_Permutation; eassumption. Qed.
imports: Coq.Lists.List Coq.Sets.Ensembles Fiat.Common Fiat.Common.List.PermutationFacts Fiat.Common.Ensembles.EnsembleListEquivalence