In this proof pearl, we demonstrate the power of higher-order encodings in the logical framework Twelf[PS99] by investigating proofs about an algorithmic specification of bounded subtype polymorphism, a problem from the POPLmark challenge [ABF+05]. Our encoding and representation of the problem plays to the strengths of the logical framework LF. Higher-order abstract syntax is used to deal with issues of bound variables. More importantly, we exploit the full advantage of parametric and higher-order judgments. As a key benefit we get a tedious narrowing lemma, which must normally be proven separately, for free. Consequently, we obtain an extremely compact and elegant encoding of the admissibility of general transitivity and other meta-theoretic properties.