proposition: Lemma wo_leq_rw : 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. ap iff_eq; ir. ap wo_avatar_ordinal_leq; try am. cp H. uh H; ee. uh H; ee. cp (H5 _ _ H0 H1). nin H6. am. assert (ordinal_leq (wo_avatar a y) (wo_avatar a x)). ap wo_avatar_ordinal_leq; try am. uh H2. uh H7. ee. assert (x = y). util (wo_avatar_injective (a:=a)). am. uh H12; ee. uh H13. ap H13. am. am. ap extensionality; am. rw H12. ap leq_refl; try am; try lu. Qed.
imports: Arith transfinite