# HG changeset patch
# User ryokka
# Date 1576914547 -32400
# Node ID 7523d5cd670b05e90336df687ede10e69c4307de
# Parent  990d1d8923989369b964508ac9b4625e988fe390
fix

diff -r 990d1d892398 -r 7523d5cd670b whileTestGears.agda
--- a/whileTestGears.agda	Sat Dec 21 16:35:54 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 16:49:07 2019 +0900
@@ -185,5 +185,4 @@
 
 {-# TERMINATING #-}
 Proof : (c :  ℕ ) → whileTestPCallwP c
-Proof zero = whileTestPwP {_} {_} zero (λ env s → refl)
-Proof (suc c) = Proof (suc c)
+Proof c = Proof c