proposition: Lemma leq_gen_ordinal : forall o:E, leq_gen ID o o -> is_ordinal o.
proof: Proof. ir. uh H. nin H; ee. assert (is_ordinal (U x)). uhg. uhg. sh x; ee; try tv; try am. apply ordinal_inc_ordinal with (U x). am. uh H0; ee; am. Qed.
imports: Arith transfinite