Preserve sizes in Definitions

[ionathanch]

Using Definition for a non-recursive but size-preserving definition does not internally annotate its type in a size-preserving way:

Definition id (x : nat) := x.
Fail Fixpoint f (n : nat) :=
  match n
  | O => O
  | S n' => f (id n')
  end.

id1 will have type nat^∞ -> nat^∞ rather than nat^ⁱ -> nat^ⁱ. We need to use Fixpoint to allow these annotations:

Fixpoint id (x : nat) := x.
Fail Fixpoint f (n : nat) :=
  match n
  | O => O
  | S n' => f (id n')
  end.

However, doing so will raise the warning Not a truly recursive fixpoint. [non-recursive,fixpoints].

We should allow Definition to also assign size-preserving types to global definitions.