--- a/whileTestGears.agda	Fri Dec 13 19:45:34 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 13 19:54:28 2019 +0900
@@ -177,15 +177,15 @@
 
 
 {-# TERMINATING #-}
-loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
-          → Pre c  → (exit : (c2 : Context) → (P c2) → Post c2  → t)
-          (f : Context → (exit : (c2 : Context) → (P c2) → Post c2  → t) → t) → t
-loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt if pre exit f = lem cxt
+loopProof : {l : Level} {t : Set l} {P Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
+           → Inv c → (exit : (c2 : Context) → (P c2) → Inv c2  → t)
+          (f : Context → (exit : (c2 : Context) → (P c2) → Inv c2  → t) → t) → t
+loopProof {l} {t} {P} {Inv} cxt if inv exit f = lem cxt inv
   where
-    lem : (c : Context) → t
-    lem c  with if c
-    lem c | no ¬p = f c exit
-    lem c | yes p = exit c p {!!}
+    lem : (c : Context) → Inv c → t
+    lem c inv with if c
+    lem c inv | no ¬p = f c (λ c1 inv1 inv2 → lem c1 {!!} )
+    lem c inv | yes p = exit {!!} {!!} {!!}