# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576996901 -32400
# Node ID bef5d4281ac81cf45f2a69fb12ab684404079066
# Parent  87e125b119997e0157e910b0173bd5fa49e968f5
...

diff -r 87e125b11999 -r bef5d4281ac8 whileTestGears.agda
--- a/whileTestGears.agda	Sun Dec 22 15:41:26 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 22 15:41:41 2019 +0900
@@ -179,8 +179,8 @@
 whileTestPwPSound :  (c : ℕ) → whileTestPwP c ( λ env s → whileTestStateP s1 env )
 whileTestPwPSound c = record { pi1 = refl ; pi2 = refl }
 
-GearsIdSound : (env : Envc) {post : Envc → Set} (f : {l : Level } {t : Set l } → Envc → ((e : Envc) → post e → t ) → t )  → f env ( λ env s → post env )
-GearsIdSound env {post} f = {!!}
+GearsIdSound : (env : Envc) {post : Envc → Set} (f : {l : Level } {t : Set l } → Envc → ((e : Envc) → post e → t ) → t )  → post (f env ( λ env s → env ))
+GearsIdSound env {post} f = ?
 
 -- hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → (vari e ≡ 0) /\ (varn e ≡ c))
 -- hoge c env = GearsIdSound env (λ e → whileTestPwP c )