proposition: Lemma ordinal_leq_gen_refl : forall o:E, is_ordinal o -> leq_gen ID o o.
proof: Proof. ir. pose (q:= tack_on o o). assert (is_ordinal q). uf q; ap ordinal_tack_on. am. uh H0. uh H0. nin H0; ee. assert (inc o (U x)). rw H0; uf q; rw tack_on_inc. ap or_intror; tv. rw (leq_gen_leq (f:=ID) (a:= x)). ap leq_refl. do 3 (uh H1; ee); am. am. am. am. am. Qed.
imports: Arith transfinite