proposition: Lemma ordinal_leq_obi : forall a x y, next_compatible ID a -> inc x (U a) -> inc y (U a) -> leq (obi (U a)) x y = leq a x y.
proof: Proof. ir. assert (is_ordinal (U a)). uhg; ee. uhg. sh a; ee; try tv; try am. ap iff_eq; ir. wr (leq_gen_leq (f:=ID)). rwi ordinal_obi_leq H3. ee. wr ordinal_leq_leq_gen. am. am. am. am. am. rw ordinal_obi_leq. ee; try am. wri (leq_gen_leq (f:=ID)) H3. rw ordinal_leq_leq_gen. am. am. am. am. am. Qed.
imports: Arith transfinite