proposition: Lemma option_subset {A} (s1 : set (option A)) : s1 \subset (isSome :&: s1) :|: [set None].
proof: Proof. intros [x |]; firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)