proposition: Lemma tnth_fgraph f i : tnth (fgraph f) i = f (enum_val i).
proof: Proof. by rewrite tnth_map /tnth -enum_val_nth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)