proposition: Lemma functor_compose_equiv `{FF : FullyFaithful F} `(G : Functor) `(H : Functor) (T : G [≅] H) : F ◌ G [≅] F ◌ H.
proof: Proof. intros. unfold Natural_Iso in *. intros. apply Functor_Congruence. assumption. Qed.
imports: Ssreflect.choice Basics Endo FCompose Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Relations.Relation_Definitions