fact: Definition finite_inv_list_covers_and_card : forall (E:set A), finite E -> exists L, list_covers E L /\ card E = length L.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)