conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
               → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
conversion1 env {c10} p1 next = next env proof4 where
      proof4 : varn env + vari env ≡ c10
      proof4 = let open ≡-Reasoning  in begin
            varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
            c10 + vari env      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
            c10 + 0             ≡⟨ +-sym {c10} {0} ⟩
            c10
          ∎