proposition: Lemma composition_of_helper : (fun x => G' o G o x o (F' o F)) = (fun x => G' o (G o x o F') o F).
proof: Proof. apply path_forall; intro x. apply composition_of_helper_helper. Defined.
imports: Category.Core Functor.Core Functor.Pointwise.Core NaturalTransformation.Core NaturalTransformation.Paths Functor.Composition.Core Functor.Identity Functor.Paths PathGroupoids Types.Forall HoTT.Tactics Basics.Tactics