proposition: Lemma tuple_uniqP (t : n.-tuple T) : reflect (injective (tnth t)) (uniq t).
proof: Proof. case: {+}n => [|m] in t *; first by rewrite tuple0; constructor => -[]. pose x0 := tnth t ord0; apply/(equivP (uniqP x0)); split=> tinj i j. by rewrite !(tnth_nth x0) => /tinj/val_inj; apply; rewrite size_tuple inE. rewrite !size_tuple !inE => im jm; have := tinj (Ordinal im) (Ordinal jm). by rewrite !(tnth_nth x0) => /[apply]-[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)