proposition: Lemma transdef_tg3 r (f: fterm): worder r -> (forall x, inc x (substrate r) -> f x = fun_image (segment r x) f) -> forall x, inc x (substrate r) -> f x = Vf (ordinal_iso r) x.
proof: Proof. move => wor pa x xX. have or := proj1 wor. set C := (fun f0 : Set => target (fgraph_to_fun f0)). rewrite /ordinal_iso /transfinite_defined -/C fgraph_to_fun_ev. pose g := Lg (substrate r) f. have ->: f x = Vg g x by rewrite LgV. congr Vg; symmetry; apply: (transfinite_pr2 wor). have fg : fgraph g by rewrite/g;fprops. rewrite /g; saw => t tX; rewrite LgV //. rewrite (pa _ tX) /C corresp_t - Lg_range restr_Lg //; apply: sub_segment. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)