proposition: Lemma card_eq_length_to_list : forall (E:set A), finite E -> card E = length (to_list E).
proof: Proof. Proof using. introv FE. applys list_repr_inv_card. applys~ eq_to_list_inv. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)