proposition: Corollary fobj_Compose `(F : D ⟶ E) `(G : C ⟶ D) {x} : fobj[F ◯ G] x = fobj[F] (fobj[G] x).
proof: Proof. reflexivity. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic