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

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