proposition: Lemma wo_punctured_downward : forall a x, is_well_ordered a -> inc x (U a) -> Image.create (punctured_downward_subset a x) (wo_avatar a) = wo_avatar a x.
proof: Proof. ir. rewrite<- chenille_punctured_downward with (f:=next a). uf wo_avatar. wr avatar_chenille. ap ordinal_chenille. change (is_ordinal (wo_avatar a x)). ap wo_avatar_is_ordinal. am. am. ap ID_expansive. rw next_leq_gen_leq. ap leq_refl; lu. am. am. am. ap next_compatible_next; am. am. Qed.
imports: Arith transfinite