1.1 --- a/src/HOL/Library/Equipollence.thy	Tue Dec 03 16:51:53 2019 +0100
     1.2 +++ b/src/HOL/Library/Equipollence.thy	Wed Dec 04 12:44:38 2019 +0000
     1.3 @@ -693,4 +693,19 @@
     1.4    apply (auto simp: finite_PiE_iff PiE_eq_empty_iff dest: not_finite_existsD)
     1.5    using finite.simps by auto
     1.6  
     1.7 +lemma lists_lepoll_mono:
     1.8 +  assumes "A \<lesssim> B" shows "lists A \<lesssim> lists B"
     1.9 +proof -
    1.10 +  obtain f where f: "inj_on f A" "f ` A \<subseteq> B"
    1.11 +    by (meson assms lepoll_def)
    1.12 +  moreover have "inj_on (map f) (lists A)"
    1.13 +    using f unfolding inj_on_def
    1.14 +    by clarsimp (metis list.inj_map_strong)
    1.15 +  ultimately show ?thesis
    1.16 +    unfolding lepoll_def by force
    1.17 +qed
    1.18 +
    1.19 +lemma lepoll_lists: "A \<lesssim> lists A"
    1.20 +  unfolding lepoll_def inj_on_def by(rule_tac x="\<lambda>x. [x]" in exI) auto
    1.21 +
    1.22  end