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