proposition: Lemma fmor_compv : forall a f u v, axioms f -> a = source f -> mor a u -> mor a v -> source u = target v -> fmor f (comp a u v) = comp (target f) (fmor f u) (fmor f v).
proof: Proof. ir. rw H0. sy. rw comp_fmor. tv. am. wr H0; am. wrr H0. am. Qed.
imports: Arith category