{-!$\#$! TERMINATING !$\#$!-}
whileLoop!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! {c10 :  !$\mathbb{N}$! } !$\rightarrow$! ((varn env) + (vari env) !$\equiv$! c10)
   !$\rightarrow$! (Code : (e1 : Env )!$\rightarrow$! vari e1 !$\equiv$! c10 !$\rightarrow$! t) !$\rightarrow$! t
whileLoop!$\prime$! env proof next with  ( suc zero  !$\leq$!? (varn  env) )
whileLoop!$\prime$! env {c10} proof next | no p = next env ( begin
       vari env            !$\equiv$!!$\langle$! refl !$\rangle$!
       0 + vari env        !$\equiv$!!$\langle$! cong (!$\lambda$! k !$\rightarrow$! k + vari env) (sym (lemma1 p )) !$\rangle$!
       varn env + vari env !$\equiv$!!$\langle$! proof !$\rangle$!
       c10 !$\blacksquare$! ) where open !$\equiv$!-Reasoning  
whileLoop!$\prime$! env {c10} proof next | yes p = whileLoop!$\prime$! env1 (proof3 p ) next where
      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
      1<0 : 1 !$\leq$! zero !$\rightarrow$! !$\bot$!
      1<0 ()
      proof3 : (suc zero  !$\leq$! (varn  env))  !$\rightarrow$! varn env1 + vari env1 !$\equiv$! c10
      proof3 (s!$\leq$!s lt) with varn  env
      proof3 (s!$\leq$!s z!$\leq$!n) | zero = !$\bot$!-elim (1<0 p)
      proof3 (s!$\leq$!s (z!$\leq$!n {n!$\prime$!}) ) | suc n =  let open !$\equiv$!-Reasoning  in begin
             n!$\prime$! + (vari env + 1)  !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n!$\prime$! + z ) ( +-sym  {vari env} {1} )  !$\rangle$!
             n!$\prime$! + (1 + vari env ) !$\equiv$!!$\langle$! sym ( +-assoc (n!$\prime$!)  1 (vari env) ) !$\rangle$!
             (n!$\prime$! + 1) + vari env  !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z + vari env )  +1!$\equiv$!suc  !$\rangle$!
             (suc n!$\prime$! ) + vari env !$\equiv$!!$\langle$!!$\rangle$!
             varn env + vari env  !$\equiv$!!$\langle$! proof  !$\rangle$!
             c10
          !$\blacksquare$!