proposition: Lemma eq_to_list_inv : forall E L, L = to_list E -> finite E -> list_repr E L.
proof: Proof. introv EQ HE. unfolds. subst. forwards* (?&?): list_repr_to_list_of_finite HE. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)