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

[Adam Chlipala]

Marc Weber wrote:
> 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.
>    

I don't think there's a good way to implement "type-level projection" 
from records.  If you share some of the context where you want to use 
such an operation, I may be able to suggest an alternate idiomatic 
technique.