 The basic idea is that a proposition in sense 1 gives rise to the problem of finding a construction that fulfills the expressed intention, and that a solution to a problem posed in a proposition in sense 2 also serves to fulfill the intention towards constructions that solve that problem; this is made fully explicit in a little argument due to Martin-Löf, given in detail in Sundholm 1983: 158–159.