proposition: Lemma allP {a s} : reflect {in s, forall x, a x} (all a s).
proof: Proof. elim: s => [|/= y s IHs]; first by left. exact: equivP (andPP idP IHs) (iff_sym forall_cons). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)