According to Martin-Löf (1982) the meaning of a hypothetical judgment is reduced to the meaning of the categorical judgments by substituting the closed terms of appropriate types for the free variables. For example, the meaning of