proposition: Lemma wo_avatar_ordinal_inc : forall a x, is_well_ordered a -> inc x (U a) -> inc (wo_avatar a x) (wo_ordinal a).
proof: Proof. ir. uf wo_ordinal. rw Image.inc_rw. sh x; ee; try am; try tv. Qed.
imports: Arith transfinite