proposition: Lemma assoc : forall a b u v w, mor a u -> mor a v -> mor a w -> source u = target v -> source v = target w -> a= b -> comp a (comp b u v) w = comp a u (comp b v w).
proof: Proof. ir. wr H4. assert (associativity_facts a u v w). ap show_associativity_facts; ap show_composable; am. uh H5; ee. sy; am. Qed.
imports: Arith universe