I was reading Foundations of Constructive Analysis by Errett Bishop, and I came across this intersting passage:

It is not strictly correct to say that a real number

isan element of . An element of consists of a real numberanda positive integer , such that , because an element of is not presented until both and are given. One and the same real number can be associated with two distinct (but equal) elements of . Nevertheless we shall continue to refer loosely to a positive real number . On those occasions when we need to refer to an for which , we shall take the position that it was there implicitly all along.

In other words, the proposition really stands for the type

of all with . Bishop does not appear to be aware of the

propositions-as-types interpretation in this book, but he uses it implicitly.