proposition: Lemma sub_has_dom (T : eqType) (s1 s2 : seq T) (p : pred T) : {subset s2 <= s1} -> has p s2 -> has p s1.
proof: Proof. move => H /hasP [x /H Hx] ?. by apply/hasP; exists x. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)