Sun Dec 16 07:32:06 JST 2018 Gears の方に term condition を入れる initial condition に変数を入れる (証明でしか計算できないようにするため) Gears 側の証明をメタ計算的にする メタ計算以外は元の計算を保存する用にする