proposition: Lemma list_covers_of_list_repr : forall E L, list_repr E L -> list_covers E L.
proof: Proof. Proof using. introv (ND&EQ). introv Hx. rewrite~ EQ. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)