Adding Size< to standard library.

Used for coinduction with copatterns, as in:
      
  record R (i : Size where
    field force : {j : Size< i} -> R j

Patch by Andreas Abel
inspect on steroids for heterogeneous equality

Patch by James Chapman