∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) [LawfulApplicative m]
  (x y : FreeAddSemigroup α), traverse F (x + y) = (fun x1 x2 => x1 + x2) <$> traverse F x <*> traverse F y