proposition: Lemma in_sub_all (T : eqType) (a1 a2 : pred T) (s : seq T) : {in s, subpred a1 a2} -> all a1 s -> all a2 s.
proof: Proof. move => sub /allP H. apply/allP => x in_s. by firstorder. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)