proposition: Lemma law : functor C1 C2 D o inverse C1 C2 D = 1 /\ inverse C1 C2 D o functor C1 C2 D = 1.
proof: Proof. split; path_functor; [ (exists (path_forall _ _ helper1)) | (exists (path_forall _ _ helper2)) ]; unfold helper1, helper2, helper2_helper; exp_laws_t. Qed.
imports: Category.Core Functor.Core Functor.Paths Functor.Identity Functor.Composition.Core ExponentialLaws.Law4.Functors ExponentialLaws.Tactics