(w: (v: _) -> v Type) -> w Type