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

[Marc Weber]

Excerpts from Gergely Buday's message of Thu Dec 15 21:18:44 +0100 2011:
> Is this not what you want?
> con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
No, you're operating on "tuples". Those examples can be found in the
tutorial.

I wondered why there is tuple.1 but not record.#A.
Because the tutorial mentions project:

  fun project [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (r : $([nm = t] ++ ts)) : t = r.nm

I wondered whether I could write a type level version of that because
there are records and type-level records you might think that there is a
way to do type level projection. I haven't found it in the manualy. I
failed rewriting the fun above as con (type-level) too.

Marc Weber