proposition: Lemma ordinal_leq_leq_gen : forall a o:E, ordinal_leq a o = leq_gen ID a o.
proof: Proof. ir. ap iff_eq; ir. assert (leq_gen ID a a). ap ordinal_leq_gen_refl. uh H; ee; am. assert (leq_gen ID o o). ap ordinal_leq_gen_refl. uh H; ee; am. cp (leq_gen_or H0 H1). nin H2. am. assert (ordinal_leq o a). ap leq_gen_ordinal_leq. am. assert (a = o). ap extensionality. uh H; ee; am. uh H3; ee; am. rw H4; am. ap leq_gen_ordinal_leq; am. Qed.
imports: Arith transfinite