 It turns out that when one is treating \(\lambda\)-calculus as a kind of programming language, one can write conditional statements “If \(P\) then \(A\) else \(B\)” simply as \(PAB\), where of course \(P, A\), and \(B\) are understood as \(\lambda\)-terms. If \(P \rhd \bT\), that is, P is ‘true’, then we have