proposition: Lemma finfun_of_tupleK : cancel finfun_of_tuple tuple_of_finfun.
proof: Proof. by move=> t; apply: eq_from_tnth => i; rewrite tnth_map ffunE tnth_ord_tuple. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)