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