@article{cockx2018,
  author={Cockz, Jesper and Devriese, Dominique},
  title={Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory},
  volume={28},
  DOI={10.1017/S095679681800014X},
  journal={Journal of Functional Programming},
  publisher={Cambridge University Press},
  year={2018},
  pages={e12}
}
