whileTestPwP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! ((env : Envc ) !$\rightarrow$! whileTestStateP s1 env !$\rightarrow$! t) !$\rightarrow$! t
whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
  env : Envc
  env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )

loopPwP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env !$\rightarrow$! t) !$\rightarrow$! t
loopPwP!$\prime$! zero env refl refl exit = exit env refl
loopPwP!$\prime$! (suc n) env refl refl exit  = whileLoopPwP!$\prime$! (suc n) env refl refl (!$\lambda$! env x y !$\rightarrow$! loopPwP!$\prime$! n env x y exit) exit


whileTestPCallwP!$\prime$! : (c :  !$\mathbb{N}$! ) !$\rightarrow$! Set
whileTestPCallwP!$\prime$! c = whileTestPwP {_} {_} c (!$\lambda$! env s !$\rightarrow$! loopPwP!$\prime$! (varn env) env refl (conv env s) ( !$\lambda$! env s !$\rightarrow$! vari env !$\equiv$! c10 env )  )