proposition: Lemma allP T P test: (forall x: T, reflect (P x) (test x)) -> forall ls, reflect (all P ls) (allb test ls).
proof: Proof. move=>H; elim=>//=[| x xs Ih]; first by constructor. case X: (test x)=>/=; last by constructor; case; move/H; rewrite X. case Y: (allb test xs); constructor. - by split; [apply/H | case: Ih Y]. by case: Ih Y=>// H1 _; case. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq)