add dummy proof to Coq script
Merge branch 'peek_file'
manually add lost file from peek_file branch
Makefile modified, PeekNext contracts modified