proposition: Lemma helper2_helper c x : inverse C1 C2 D (functor C1 C2 D c) x = c x.
proof: Proof. path_functor. abstract exp_laws_t. Defined.
imports: Category.Core Functor.Core Functor.Paths Functor.Identity Functor.Composition.Core ExponentialLaws.Law4.Functors ExponentialLaws.Tactics