[Ur] where to put disjointness proof when concatenating two type level records?

[Marc Weber]

con con_type_level_record = fn (n :: Name) (n2 :: Name) (t :: Type) (t2 :: Type) => [n = t, n2 = t2]

main.ur|141 col 84| 141:100: Couldn't prove field name disjointness
||     Con 1:  [n = ()]
||     Con 2:  [n2 = ()]
|| Hnormed 1:  [n = ()]
|| Hnormed 2:  [n2 = ()]

Can this be done ?

Probably it should look like this: [[n] ~ [n2]]

Marc Weber