whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
  env : Envc
  env = whileTestP c10 ( λ env → env )

loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
loopPwP' zero env refl refl exit = exit env refl
loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit


whileTestPCallwP' : (c :  ℕ ) → Set
whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env )  )