In this paper we relate the lax modality O to Intuitionistic Propositional Logic and give a complete characterisation of inhabitation in Computational Type Theory as a logic of constraint contexts. This solves a problem open since the 1940's, when Curry was the first to suggest a formal syntactic interpretation of O in terms of contexts.