package coq-ptsatr
PTSATR
Install
Dune Dependency
Authors
Maintainers
Sources
v8.5.0.tar.gz
md5=4ba0c590baf4df955e3440ca456440ce
Description
Formalization of the proof that PTS and PTS with judgmental equality (PTSe) are equivalent. With this equivalence, we are able to derive all the meta-theory of PTSe, like Pi-injectivity or Subject Reduction.
On This Page