Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory

Cockx, JesperJesperCockxDevriese, DominiqueDominiqueDevriese2021-10-252021-10-2520180956-7968https://imec-publications.be/handle/20.500.12860/30446Proof-relevant unification: Dependent pattern matching with only the axioms of your type theoryJournal articlehttps://doi.org/10.1017/S095679681800014X