No description
| theories | ||
| .gitignore | ||
| _CoqProject | ||
| Makefile | ||
| README.md | ||
| syntax.sig | ||
This repository contains a proof of pi injectivity for an untyped equational theory with surjective pairing and extensionality.
| theories | ||
| .gitignore | ||
| _CoqProject | ||
| Makefile | ||
| README.md | ||
| syntax.sig | ||
This repository contains a proof of pi injectivity for an untyped equational theory with surjective pairing and extensionality.