--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda-mcg.agda.replaced	Tue Nov 02 06:55:58 2021 +0900
@@ -0,0 +1,5 @@
+whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@
+             ((env : Envc ) @$\rightarrow$@ (mdg : (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)) @$\rightarrow$@ t) @$\rightarrow$@ t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+  env : Envc
+  env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )