whileTestP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! (Code : Envc !$\rightarrow$! t) !$\rightarrow$! t
whileTestP c10 next = next (record {c10 = c10 ; varn = c10 ; vari = 0 })

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

{-!$\#$! TERMINATING !$\#$!-}
loopP : {l : Level} {t : Set l} !$\rightarrow$! Envc !$\rightarrow$! (exit : Envc !$\rightarrow$! t) !$\rightarrow$! t
loopP env exit = whileLoopP!$\prime$! env (!$\lambda$! env !$\rightarrow$! loopP env exit ) exit

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

-- whileTestPCall 10
-- record { c10 = 10 ; varn = 0 ; vari = 10 }