fibers of first projection

[DanGrayson]

This lemma is rather special, and gets used only to show that we can form an injection from a predicate. Perhaps we should just prove more generally the the fibers are the first projection are equivalent to the members of the family, for any family of types used to form a sum-type. Or do we already do that somewhere?

[UlrikBuchholtz]

We have that later in Lemma 2.24.1 (lem:fst-fiber(a)=B(a)).