loopP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! Envc !$\rightarrow$! (exit : Envc !$\rightarrow$! t) !$\rightarrow$! t
loopP!$\prime$! record { c10 = c10 ; varn = zero ; vari = vari } exit =
  exit (record { c10 = c10 ; varn = zero ; vari = vari })
loopP!$\prime$! record { c10 = c10 ; varn = (suc varn!$\_{1}$!) ; vari = vari } exit =
  whileLoopP!$\prime$! (record { c10 = c10 ; varn = (suc varn!$\_{1}$!) ; vari = vari })
  (!$\lambda$! env !$\rightarrow$! loopP!$\prime$! (record { c10 = c10 ; varn = varn!$\_{1}$! ; vari = vari }) exit ) exit

whileTestPCall!$\prime$! : (c10 :  !$\mathbb{N}$! ) !$\rightarrow$! Envc
whileTestPCall!$\prime$! c10 = whileTestP!$\prime$! {_} {_} c10 (!$\lambda$! env !$\rightarrow$! loopP!$\prime$! env (!$\lambda$! env !$\rightarrow$!  env))

-- whileTestP!$\prime$! 10
-- record { c10 = 10 ; varn = 0 ; vari = 10 }