  We develop an extension of the proof environment Beluga with datasort
refinement types and study its impact on mechanized proofs. In particular, we
introduce refinement schemas, which provide fine-grained classification for the
structures of contexts and binders. Refinement schemas are helpful in concisely
representing certain proofs that rely on relations between contexts. Our
formulation of refinements combines the type checking and sort checking phases
into one by viewing typing derivations as outputs of sorting derivations. This
allows us to cleanly state and prove the conservativity of our extension.
