whileTestPSem :  (c : ℕ) → whileTestP c
  ( λ env → ⊤ implies (vari env ≡ 0) ∧ (varn env ≡ c10 env) )
whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )