 Brouwer’s proof of the bar theorem from 1924 (later versions of the proof appeared in 1927 and in 1954) proves a statement of the form “If \(A\) has been demonstrated, then \(B\) is demonstrable” (Brouwer 1924D1, 1927B, 1954A). This would evidently not be an implication \(A \rightarrow B\) if the latter were understood as a transformation of the proof conditions of \(A\) into those of \(B\), because in the former case there is the additional information that, by hypothesis, \(A\) has been demonstrated. In other words, we have, by hypothesis, a concrete proof of \(A\) at hand. (However, both are hypothetical judgements in the sense that neither requires that we actually have demonstrated \(A\).) It may be possible to exploit this extra information, and below it will be indicated how Brouwer did this. (Heyting in 1956 also chose to understand implication in this stronger sense, that is, in terms of assertion conditions; see  section 5.4  below.)