whileCallwP : (c : !$\mathbb{N}$!) !$\rightarrow$! whileTestPCallwP!$\prime$! c
whileCallwP c = whileTestPwP {_} {_} c
  (!$\lambda$! env s !$\rightarrow$! loopPwP!$\prime$! (c10 env) env (sym (pi2 s)) (conv env s) {!!})


-- Goal: (env!$\_{1}$! : Envc) !$\rightarrow$!
--        vari env!$\_{1}$! !$\equiv$! c10 env!$\_{1}$! !$\rightarrow$!
--        loopPwP!$\prime$! c (whileTestP c (!$\lambda$! env!$\_{2}$! !$\rightarrow$! env!$\_{2}$!)) refl +zero
--        (!$\lambda$! env!$\_{2}$! s!$\_{1}$! !$\rightarrow$! vari env!$\_{2}$! !$\equiv$! c10 env!$\_{2}$!)
-- ————————————————————————
-- s   : (vari env !$\equiv$! 0) !$\wedge$! (varn env !$\equiv$! c10 env)
-- env : Envc
-- c   : !$\mathbb{N}$!