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

[Gergely Buday]

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

Is this not what you want?

con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2

- Gergely