TY - RPRT TI - Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search AU - Zachary Snow AU - David Baelde AU - Gopalan Nadathur PY - 2010 UR - https://arxiv.org/abs/1007.0779 ID - 1007.0779 ER -