proposition: Lemma are_composable_create_rw : forall o m c i s u v, are_composable (create o m c i s) u v = (inc u m & inc v m & source u = target v).
proof: Proof. ir. ap iff_eq; ir. uh H. rwi is_mor_create H. rwi is_mor_create H. xd. uhg. do 2 (rw is_mor_create). xd. Qed.
imports: Arith universe