proposition: Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | s = map sval s'}.
proof: Proof. elim: s => /= [_|x s ihs /andP [ax /ihs [s' ->]]]; first by exists [::]. by exists (exist a x ax :: s'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)