[Ur] disjointness proof in type-level functions

[Sergey Mironov]

Hi. I faced a problem while exploring the type system. Looks like I
can't define a constructor-level function which adds a field (of int
type) to the record. I've tried to do the following:

> con addIntField = fn (n :: Name) (t::{Type}) => [n = int] ++ t

Ur complains about missing disjointness proof. I understand what it
is, but what I don't know it how to add this proof. Is it ever
possible on this level? All examples I've seen so far have such proof
on value-level, like 'project' function from [1]. I need this to teach
my app to define tables for custom records, adding primary key named
Id, like

con c_users = [ Name = string, Pass = string]

..

table users : $(addIntField #Id c_users) PRIMARY KEY Id

Regards,
Sergey

[1] - http://www.impredicative.com/ur/tutorial/tlc.html