Feature: support constructor arguments given as binders

[alexkeizer]

In a regular inductive I can define arguments to a constructor by defining binders in front of the :. Currently, in data or codata this is not accepted: all arguments have to be declared by giving an arrow type after the semi-colon. We should add support for binders.

-- This currently works
data Wrap α
  | mk : α → Wrap α

-- This should work, too, and give an equivalent type
data Wrap₂ α
  | mk (a : α) : Wrap₂ α
--     ^^^^^^^ Notice how the `α` argument has been moved in front of the semi-colon

-- Also, note we shouldn't have to give the type of the constructor if it's trivial, 
-- The following should work, too:
data Wrap₃ α
  | mk (a : α)