Safe Proof Checking in Type Theory with Y: Examples

In the article Safe Proof Checking in Type Theory with Y, to appear in CSL'99, we give two examples. This page gives the input to Coq for concrete versions of these examples. We used the following version of Coq: Coq V6.2.4 (January 1999).