translation of GoedelGod_theorem_1_oneStep.p (THF0) into Isabelle syntax