proposition: Lemma finite_inj_submseteq `{finA: Finite A} `{finB: Finite B} (f: A → B) `{!Inj (=) (=) f} : f <$> enum A ⊆+ enum B.
proof: Proof. intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2. Qed.
imports: stdpp(options)