proposition: Lemma isSome_subset {A : Type} (s1 s2 s1' s2' : set (option A)) : isSome :&: s1 \subset isSome :&: s2 -> isSome :&: (s1 :|: ([set None] :&: s1')) \subset isSome :&: (s2 :|: ([set None] :&: s2')).
proof: Proof. intros Hyp x [H1 H2]. destruct x as [ x | ]; try discriminate. split; eauto. inv H2. left; eauto. eapply Hyp. now split; eauto. inv H. now inv H0. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)