Create nCkList.v

work as much as possible by retracting the trivial construction on function types.