proposition: Lemma tuple0 : all_equal_to ([tuple] : 0.-tuple T).
proof: Proof. by move=> t; apply: val_inj; case: t => [[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)