proposition: Lemma helper (c : Functor D C1 * Functor D C2) : ((fst o (Datatypes.fst c * Datatypes.snd c))%functor, (snd o (Datatypes.fst c * Datatypes.snd c))%functor)%core = c.
proof: Proof. apply path_prod; [ apply compose_fst_prod | apply compose_snd_prod ]. Defined.
imports: Category.Core Functor.Core Functor.Prod Functor.Paths Functor.Identity Functor.Composition.Core ExponentialLaws.Law3.Functors Types.Prod ExponentialLaws.Tactics