Verifying Uniqueness in a Logical Framework

We present an algorithm for verifying that some specified arguments of an inductively defined relation in a dependently typed lambda-calculus are uniquely determined by some other arguments. We prove it correct and also show how to exploit this uniqueness information in coverage checking, which allows us to verify that a definition of a function or relation covers all possible cases. In combination, the two algorithms significantly extend the power of the meta-reasoning facilities of the Twelf implementation of LF.