proposition: Lemma show_composable : forall c u v, mor c u -> mor c v -> source u = target v -> composable c u v.
proof: Proof. ir. cp H; uh H; ee. cp H; uh H; ee. uhg; ee. am. uh H0; ee. uhg; ee; try am. Qed.
imports: Arith universe