proposition: Lemma list_repr_nil: list_repr \{} (@nil A).
proof: Proof. Proof using. rewrite <- to_list_empty. eapply eq_to_list_inv; eauto using finite_empty. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)