proposition: Lemma sub_all_dom (T : eqType) (s1 s2 : seq T) (p : pred T) : {subset s1 <= s2} -> all p s2 -> all p s1.
proof: Proof. move => sub /allP H. apply/allP => x /sub. exact: H. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)