proposition: Lemma fgraphE T (r1 r2 : {ffun I -> T}) : fgraph r1 = fgraph r2 -> r1 = r2.
proof: Proof. by move=> eq_r12; apply/ffunP=> x; rewrite -[x]enum_rankK -!tnth_fgraph eq_r12. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap) mathcomp(fintype tuple finfun)