proposition: Lemma transfinite_def_prop1 r T f: transfiniteg_def r T f <-> transfinite_def r (T \o graph) (fgraph_to_fun f).
proof: Proof. split. move => [ha hb hc]; split. - by apply:fgraph_to_fun_fs. - by rewrite fgraph_to_fun_source. - move => x xsr; rewrite fgraph_to_fun_ev (hc _ xsr). by rewrite /restriction1/fgraph_to_fun/=; aw. move => [[ff _] hb hc]; split. - by move: (proj32 ff); rewrite /fgraph_to_fun; aw. - by rewrite - hb; rewrite /fgraph_to_fun; aw. - move => x xsr. move: (hc x xsr); rewrite fgraph_to_fun_ev /restriction1/fgraph_to_fun /=. by aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)