This repository contains a cleaned up version of the work done in Nottingham under Thorsten Altenkirch's supervision.
It is based on Amine Chaieb and Tobias Nipkow's formalization of a similar procedure in HOL.
This development has been typechecked with:
- Agda version 2.6.0.1
- the standard library v1.2