proposition: Lemma otrans_pr a f T: ordinalp a -> otrans_def a T f -> otrans_defined a T = f.
proof: Proof. move => ox H. move:(ordinal_o_wor ox) => wo . by apply:(transfinite_pr wo); move/(otrans_def_prop _ _ ox):H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)