proposition: Lemma wo_lt_rw : forall a x y, is_well_ordered a -> inc x (U a) -> inc y (U a) -> lt a x y = ordinal_lt (wo_avatar a x) (wo_avatar a y).
proof: Proof. ir. ap iff_eq; ir. uhg; ee. wr wo_leq_rw. uh H2; ee; am. am. am. am. uhg; ir. uh H2; ee. ap H4. util (wo_avatar_injective (a:= a)). am. uh H5; ee. ap H6. am. am. am. uhg; ee. rw wo_leq_rw. uh H2; ee; am. am. am. am. uhg; ir. uh H2. ee. ap H4. rw H3; tv. Qed.
imports: Arith transfinite