proposition: Lemma all_predI a1 a2 s : all (predI a1 a2) s = all a1 s && all a2 s.
proof: Proof. apply: (can_inj negbK); rewrite negb_and -!has_predC -has_predU. by apply: eq_has => x; rewrite /= negb_and. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)