initial.coq