proposition: Lemma wo_avatar_injective : forall a, is_well_ordered a -> Transformation.injective (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. transitivity (avatar ID (next a) (wo_avatar a x)). uf wo_avatar. rw avatar_trans. rw avatar_refl. tv. rw next_leq_gen_leq. ap leq_refl; lu. am. am. am. ap ID_expansive. rw next_leq_gen_leq. ap leq_refl; lu. am. am. am. rw H2. uf wo_avatar. rw avatar_trans. rw avatar_refl. tv. rw next_leq_gen_leq; try am. ap leq_refl; lu. ap ID_expansive. rw next_leq_gen_leq; try am. ap leq_refl; lu. Qed.
imports: Arith transfinite