cal finfun_subType := Eval hnf in [newType for fgraph].

  Notation "{ 'ffun' fT }" := (finfun_of (Phant fT)).
End FinFunDef.

Definition fun_of_fin aT rT f x := tnth (@fgraph aT rT f) (enum_rank x).
Coercion fun_of_fin : finfun_type >-> Funclass.
Definition finfun aT rT f := @Finfun aT rT (codom_tuple f).
Notation "[ ’ffun’ x : aT => F ]" := (finfun (fun x : aT => F)).  

Check [ffun i : 'I_4 => i + 2]. (* : {ffun 'I_4 -> nat} *)

Inductive tree3 := Leaf of nat | Node of {ffun 'I_3 -> tree3}.

Definiti