proposition: Lemma imset_in a b x (f : a -> b) (A : set a) : x \in A -> f x \in (f @: A).
proof: Proof. intros. unfold imset. exists x. split; by []. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)