Callaghan, P., Luo, Zhaohui, "An implementation of LF with coercive subtyping & universes", Journal of Automated Reasoning, 2001