proposition: Lemma list_repr_inv_card : forall (E:set A) (L:list A), list_repr E L -> card E = length L.
proof: Proof. Proof using. introv HR. lets (ND&EQ): HR. forwards~ (L'&(ND'&HR')&EQ'): finite_inv_list_repr_and_card E. applys* finite_of_list_repr. unfold card. simpl. rewrite EQ'. applys~ noduplicates_length_eq. intros x. rewrite EQ. rewrite* HR'. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)