proposition: Lemma imset_incl {T U} (A B : set T) (f : T -> U): A \subset B -> f @: A \subset f @: B.
proof: Proof. move => H u [x [H1 H2]]. eexists; split; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)