proposition: Lemma wo_avatar_surjective : forall a, is_well_ordered a -> Transformation.surjective (U a) (wo_ordinal a) (wo_avatar a).
proof: Proof. ir. uhg; ee. uhg. ir. uf wo_ordinal; rw Image.inc_rw. sh x; ee; try am. tv. uhg. ir. ufi wo_ordinal H0; rwi Image.inc_rw H0. nin H0. ee. sh x0; ee; am. Qed.
imports: Arith transfinite