{-# TERMINATING #-}
whileLoop' : {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' env proof next with  ( suc zero  !$\leq$!? (varn  env) )
whileLoop' 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' env {c10} proof next | yes p = whileLoop' 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'}) ) | suc n =  let open !$\equiv$!-Reasoning  in begin
             n' + (vari env + 1)  !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n' + z ) ( +-sym  {vari env} {1} )  !$\rangle$!
             n' + (1 + vari env ) !$\equiv$!!$\langle$! sym ( +-assoc (n')  1 (vari env) ) !$\rangle$!
             (n' + 1) + vari env  !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z + vari env )  +1!$\equiv$!suc  !$\rangle$!
             (suc n' ) + vari env !$\equiv$!!$\langle$!!$\rangle$!
             varn env + vari env  !$\equiv$!!$\langle$! proof  !$\rangle$!
             c10
          !$\blacksquare$!