Added assertions as defthms.  Debugging generated ACL2.