--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/cbc-hoare-soundness.agda.replaced	Mon Mar 09 11:25:49 2020 +0900
@@ -0,0 +1,6 @@
+whileCallwP : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestPCallwP' c
+whileCallwP c = whileTestPwP {_} {_} c
+  (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!})
+  where
+    conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env
+    conv e record { pi1 = refl ; pi2 = refl } = +zero