proposition: Lemma target_comp : forall a u v, mor a u -> mor a v -> source u = target v ->target (comp a u v) = target u.
proof: Proof. ir. assert (composable_facts a u v). ap show_composable_facts; am. lu. Qed.
imports: Arith universe