Proof of Church-Rosser in Martin-Löf's Type Theory This repository houses a small Coq proof that the Church-Rosser theorem holds for Martin-Löf's intuitionistic theory of types. Building $ coq_makefile -f _CoqProject -o Makefile $ make