whileCallwP : (c : ℕ) → whileTestPCallwP' c
whileCallwP c = whileTestPwP {_} {_} c
  (λ env s → loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!})


-- Goal: (env₁ : Envc) →
--        vari env₁ ≡ c10 env₁ →
--        loopPwP' c (whileTestP c (λ env₂ → env₂)) refl +zero
--        (λ env₂ s₁ → vari env₂ ≡ c10 env₂)
-- ————————————————————————
-- s   : (vari env ≡ 0) /\ (varn env ≡ c10 env)
-- env : Envc
-- c   : ℕ