Build unfolded versions of the primitive projection in let (a, p) := ...
to maintain compatibility (HoTT bug #557).