whileTestPwP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$!
             ((env : Envc ) !$\rightarrow$! (mdg : (vari env !$\equiv$! 0) !$\wedge$! (varn env !$\equiv$! c10 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 )