proposition: Lemma R_ob_lift : forall d x (H:ob (catyd d) x), R (ob_lift H) = x.
proof: Proof. ir. assert (ob (catyd d) x). am. uh H0; ee. ufi catyd H1. rwi Category.is_ob_create H1. assert (ob_lift H = B H1). uf ob_lift. ap B_irrelevant. tv. rw H2. rw B_eq. tv. Qed.
imports: Arith cat_examples cardinal fc_limits