fact: Definition list_covers_inv_card : forall (E:set A) L, list_covers E L -> (card E <= length L)%nat.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)