conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 :  @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10)
               @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t
conversion1 env {c10} p1 next = next env proof4 where
      proof4 : varn env + vari env @$\equiv$@ c10
      proof4 = let open @$\equiv$@-Reasoning  in begin
            varn env + vari env @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ n + vari env ) (pi2 p1 ) @$\rangle$@
            c10 + vari env      @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ c10 + n ) (pi1 p1 ) @$\rangle$@
            c10 + 0             @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@
            c10
          @$\blacksquare$@