projecting from opaque pair

[ecavallo]

data unit where
| triv

opaque
let t : (A : type) × A = (unit, triv)

let a = t .snd

raises Failure("popl: empty"). Writing

let a : t .fst = t .snd

works fine.