proposition: Lemma unique : a * b = F.
proof: Proof. path_functor. exists (path_forall _ _ unique_helper). apply unique_helper2. Defined.
imports: Category.Core Functor.Core Category.Prod Functor.Composition.Core Functor.Prod.Core Functor.Paths Types.Prod HoTT.Tactics Types.Forall Types.Sigma Basics.Tactics