proposition: Lemma transfinite_defined_pr r T: worder r -> transfinite_def r T (transfinite_defined r T).
proof: Proof. move=> wo; rewrite /transfinite_defined. set T' := (fun f : Set => T (fgraph_to_fun f)). move/ (transfinite_def_prop1 ):(transfinite_pr1 T' wo). set f := fgraph_to_fun _. move => [ha hb hc]; split => // x xsr; rewrite (hc _ xsr) /T'. have ss: sub (segment r x) (source f) by rewrite hb; apply: sub_segment. by rewrite (fgraph_to_fun_restr (proj1 ha) ss) {2}/fgraph_to_fun/=; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)