proposition: Lemma transfinite_pr r x T: worder r -> transfinite_def r T x -> transfinite_defined r T = x.
proof: Proof. move => wo td; exact:(transfinite_unique wo (transfinite_defined_pr T wo) td). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)