proposition: Lemma wo_avatar_ordinal_leq : forall a x y, is_well_ordered a -> inc x (U a) -> inc y (U a) -> leq a x y -> ordinal_leq (wo_avatar a x) (wo_avatar a y).
proof: Proof. ir. uf wo_avatar. ap leq_gen_ordinal_leq; try am. ap avatar_leq_gen; try am. ap ID_expansive. rw next_leq_gen_leq; try am. Qed.
imports: Arith transfinite