@misc{indiciae0dac6fb091ac,
  title = {Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search},
  author = {Zachary Snow and David Baelde and Gopalan Nadathur},
  year = {2010},
  url = {https://arxiv.org/abs/1007.0779},
  note = {Source identifier: 1007.0779}
}