{-@$\#$@ 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$@