 Treating quantified NPs as terms for properties of properties means they can occur as arguments to any expression defined for properties of properties. We can even rescue the uncomprehending student’s attempt at ‘Jack hit someone’, for provided ‘hit’ is of the right type — which is easily arranged — we can have (hit(someone))(jack). Here hit accepts the property of being a property of at least one person, and produces the first-order property of hitting someone, which is then attributed to Jack. In extensional type-theory, hit has the type ((ib)b)(ib) if (hit(someone))(jack) is well-typed and jack is of type  i.[6]