In the conclusion of the famous “Propositions as Types” [1], Philip Wadler says the following concerning the usage of the