\section{Code Gearに合わせた Agda}
検証を行うために，AgdaのコードもCbCに合わせて記述を行う必要がある．
実際に以下がコードとなる．

CbCの特徴である，変数を継続して実行するために，必要な変数は Envc に格納する．
コードに (next : Envc → t) と (exit : Envc → t) を引数に受け取っている．
これで次の遷移先を引数として受け取る事で，実行を継続していることを示す．
= の後は next Envc もしくは exit Envc となっていることからも
実行を継続している事が分かる．