proposition: Lemma worder_numerable_bis r: worder r -> numeration r (graph (ordinal_iso r)).
proof: Proof. move=> wor. move: (transfinite_defined_pr target wor) => [suf sf vf]. have ff:= proj1 suf. hnf; rewrite (domain_fg ff) sf; split; fprops. move=> x xsr; move: (vf _ xsr); rewrite /Vf; move=> ->; apply:corresp_t. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)