proposition: Lemma create_like : forall o m c i s, like (create o m c i s).
proof: Proof. ir. uf like. ap create_extensionality. rw objects_create; tv. rw morphisms_create; tv. ir. uf comp. rw composition_create. rw create_V_rewrite. rw create_V_rewrite. tv. Ztac. am. ir. uf id. rw identity_create. rw create_V_rewrite. tv. am. rw structure_create. tv. Qed.
imports: Arith universe