proposition: Lemma transfiniteg_unique r T : worder r -> uniqueness (transfiniteg_def r T).
proof: Proof. move=> wo f f' [fgf df fv] [fgf' df' fv']. case:(worder_prop2 (fun t => Vg f t = Vg f' t) wo) => hyp. by apply: fgraph_exten => //; [ ue | move => t ts /=]; apply: hyp; ue. move:hyp => [a [asr h zp]]; case:h. rewrite (fv _ asr) (fv' _ asr); congr T; apply: restr_exten => t/segmentP lta. by apply: zp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)