proposition: Lemma imset_singl_incl {U T : Type} (x : U) (f : U -> T) : f @: [set x] \subset [set (f x)].
proof: Proof. intros y Hin. destruct Hin as [y' [Hin1 Hin2]]. inv Hin1. inv Hin2. reflexivity. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)