proposition: Lemma fcompose_assoc : forall f g h, axioms f -> axioms g -> axioms h -> source f = target g -> source g = target h -> fcompose (fcompose f g) h = fcompose f (fcompose g h).
proof: Proof. ir. uf fcompose. ap Umorphism.associativity. uhg; ee; try am. ap functor_umorphism_axioms. am. app functor_umorphism_axioms. uhg; ee; try am. app functor_umorphism_axioms. app functor_umorphism_axioms. Qed.
imports: Arith category