proposition: Lemma ordinal_obi_leq : forall x u v:E, is_ordinal x -> leq (obi x) u v = (inc u x & inc v x & ordinal_leq u v).
proof: Proof. ir. rw obi_leq; uf ordinal_leq; ap iff_eq; ir; xd. apply ordinal_inc_ordinal with x; am. apply ordinal_inc_ordinal with x; am. Qed.
imports: Arith transfinite