For a sum type inductive foo (α : Type) | foo1 : list α → ℕ → foo | ...
traverse_constructor `foo1 `foo appl_inst f `α `β [`(x : list α), `(y : ℕ)]
synthesizes foo1 <$> traverse f x <*> pure y.
derive the traverse definition of a traversable instance