requested by and OK naddy@
From: Yozo Toda <yozo@v007.vaio.ne.jp>
Submitted by Yozo Toda <yozo@imit.chiba-u.ac.jp>. The Coq Proof Assistant is designed to write formal specifications, programs and to verify that programs are correct with respect to their specification.