proposition: Lemma identity_of_helper_helper (x : Functor C D) : 1 o x o 1 = x.
proof: Proof. path_functor. 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