proposition: Lemma all_inP (T : eqType) (s : seq T) p q : reflect {in s, subpred p q} (all (fun x => p x ==> q x) s).
proof: Proof. by apply: (iffP allP) => H x /H /implyP. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)