proposition: Lemma fmor_fcompose : forall f g u, axioms f -> axioms g -> source f = target g -> mor (source g) u -> fmor (fcompose f g) u = fmor f (fmor g u).
proof: Proof. ir. uf fcompose. uf compose. rw fmor_create. tv. am. Qed.
imports: Arith category