proposition: Lemma transdef_tg1 r (f := ordinal_iso r): worder r -> forall x, inc x (substrate r) -> Vf f x = Vfs f (segment r x).
proof: Proof. move => wor x xsr. move: (transfinite_defined_pr target wor)=> [pa pb pc]. by rewrite (pc _ xsr) corresp_t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)