proposition: Lemma wo_avatar_bijective : forall a, is_well_ordered a -> Transformation.bijective (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. ap wo_avatar_surjective; am. ap wo_avatar_injective; am. Qed.
imports: Arith transfinite