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

[Marc Weber]

I remembered correctly: The wiki talks about it:
http://www.impredicative.com/wiki/index.php/Disjointness_fun_-_creating_records_using_type_level_functions
quote "
    Constructing a record type taking two names and two types. Because
    disjointness can't be proofed at type level it must be done at
    expression level.
"

My goal was to write a type level projection function - but looks like I
can't do it for this reason.

Marc Weber