proposition: Lemma wo_avatar_is_ordinal : forall a x, is_well_ordered a -> inc x (U a) -> is_ordinal (wo_avatar a x).
proof: Proof. ir. uf wo_avatar. ap leq_gen_ordinal. ap avatar_leq_gen_def. rw next_leq_gen_leq; try am. ap leq_refl; lu. Qed.
imports: Arith transfinite