proposition: Lemma onth_codom {n} (i : 'I_n) (f: {ffun 'I_n -> A}) : onth (fgraph f) i = Some (f i).
proof: Proof. pose i' := cast_ord (esym (card_ord n)) i. move: (@tnth_fgraph _ _ f i'); rewrite (enum_val_ord) {2}/i' cast_ordKV=><-. by rewrite (onth_tnth (fgraph f) i'). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)