proposition: Lemma wo_avatar_obi_id : forall o x, is_ordinal o -> inc x o -> wo_avatar (obi o) x = x.
proof: Proof. ir. cp (ordinal_obi_next_compatible H). uf wo_avatar. rewrite<- next_compatible_avatar with (f:=ID). ap avatar_refl. ap ordinal_leq_gen_refl. apply ordinal_inc_ordinal with o; am. am. rw obi_U. am. Qed.
imports: Arith transfinite