Support inductive relations where `Nat` literals appear in the type of constructors

[ngernest]

Right now, we expect any Nats that appear in the constructors of inductive relations to be expressed either as .zero or .succ (.succ ...). For example, note how in Test/DeriveArbitrarySuchThat/DeriveBalancedTreeGenerator.lean, we have to write balancedTree (.succ .zero) .Leaf instead of balancedTree 1 .Leaf:

-- `balancedTree n t` describes whether the tree `t` of height `n` is *balanced*, 
-- i.e. every path through the tree has length either `n` or `n-1`. -/
inductive balancedTree : Nat → BinaryTree → Prop where
  | B0 : balancedTree .zero BinaryTree.Leaf
  | B1 : balancedTree (.succ .zero) BinaryTree.Leaf
  | ...

It would be nice if we could allow the user to write Nat literals in the type of constructors, and somehow unfold those Nat literals to a definitionally-equal Nat expression (i.e. 2 gets unfolded to .succ (.succ .zero)) when processing the inductive relation in DeriveConstrainedProducer.lean.