proposition: Lemma transfinite_pr2 r x T: worder r -> transfiniteg_def r T x -> transfiniteg_defined r T = x.
proof: Proof. move=> wo td; exact:(transfiniteg_unique wo (transfinite_pr1 T wo) td). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)