proposition: Lemma ordinal_chenille : forall o, is_ordinal o -> chenille ID o = o.
proof: Proof. ir. ap extensionality; uhg; ir. rwi chenille_inc H0. wri ordinal_inc H0. am. am. rwi chenille_inc H0. ap ordinal_leq_gen_refl; am. ap ordinal_leq_gen_refl; am. rw chenille_inc. rwi ordinal_inc H0. am. am. ap ordinal_leq_gen_refl; am. Qed.
imports: Arith transfinite