proposition: Lemma tuple_eta n T (t : n.+1.-tuple T) : t = [tuple of thead t :: behead t].
proof: Proof. by case/tupleP: t => x t; apply: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)