proposition: Lemma forallb_tnth a t : [forall i, a (tnth t i)] = all a t.
proof: Proof. apply: negb_inj; rewrite -has_predC -has_map negb_forall. apply/existsP/(has_nthP true) => [[i a_t_i] | [i lt_i_n a_t_i]]. by exists i; rewrite ?size_tuple // -tnth_nth tnth_map. rewrite size_tuple in lt_i_n; exists (Ordinal lt_i_n). by rewrite -tnth_map (tnth_nth true). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)