proposition: Lemma helper2_helper (c : Functor (C1 + C2) D) x : (1 o c o inl C1 C2 + 1 o c o inr C1 C2) x = c x.
proof: Proof. destruct x; reflexivity. Defined.
imports: Functor.Core Category.Sum Functor.Sum Functor.Paths Functor.Identity Functor.Composition.Core Types.Prod ExponentialLaws.Tactics ExponentialLaws.Law2.Functors