proposition: Lemma imset_isSome {A} (s : set A) : Some @: s \subset isSome.
proof: Proof. intros y [x [Sx H]]. inv H. eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)