--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/cbc-hoare-soundness.agda	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,13 @@
+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   : ℕ