loopHelper : (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (eq : varn env !$\equiv$! n) !$\rightarrow$! (seq : whileTestStateP s2 env)
           !$\rightarrow$! loopPwP!$\prime$! n env (sym eq) seq (!$\lambda$! env!$\_{1}$! x !$\rightarrow$! (vari env!$\_{1}$! !$\equiv$! c10 env!$\_{1}$!))
loopHelper zero env eq refl rewrite eq = refl
loopHelper (suc n) env refl refl =
           loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))