--- a/whileTestGears.agda	Fri Dec 14 19:34:16 2018 +0900
+++ b/whileTestGears.agda	Fri Dec 14 19:51:54 2018 +0900
@@ -64,7 +64,7 @@
 -- stmt2Cond : {l : Level} → EnvWithCond {l} → 
 -- stmt2Cond env = (Equal (varn' env) 10) ∧ (Equal (vari' env) 0)
 
-whileTest' :  {t : Set}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) -> t) -> t
+whileTest' : {l : Level} {t : Set l}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) -> t) -> t
 whileTest' next = next env proof2
   where
     env : Env
@@ -73,18 +73,18 @@
     proof2 = record {pi1 = refl ; pi2 = refl}
     
 {-# TERMINATING #-}
-whileLoop' : {t : Set} -> (env : Env) -> ((vari env) + (vari env) ≡ 10) -> (Code : Env -> t) -> t
+whileLoop' : {l : Level} {t : Set l} -> (env : Env) -> ((varn env) + (vari env) ≡ 10) -> (Code : Env -> t) -> t
 whileLoop' env proof next with lt 0 (varn  env)
 whileLoop' env proof next | false = next env 
 whileLoop' env proof next | true = whileLoop' env1 proof3 next
     where
       env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
-      proof3 : vari env1 + vari env1 ≡ 10
+      proof3 : varn env1 + vari env1 ≡ 10
       proof3 = {!!}
 
-conversion1 : {t : Set} → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
-              -> (Code : (env1 : Env) -> (vari env1 + vari env1 ≡ 10) -> t) -> t
+conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
+               -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ 10) -> t) -> t
 conversion1 = {!!}
 
--- proofGears : whileLoop' {!!} {!!} {!!}
--- proofGears = {!!}
+proofGears : whileTest' (λ n →  conversion1 n {!!} (λ n1 → whileLoop' n1 {!!}  (λ n2 → (vari n2) ≡ 10)))
+proofGears = {!!}