proposition: Lemma ordinal_downward_lgs : forall o:E, is_ordinal o -> downward_lgs ID o = tack_on o o.
proof: Proof. ir. wr chenille_tack_on. rw ordinal_chenille. tv. am. ap ordinal_leq_gen_refl; am. Qed.
imports: Arith transfinite