Agda の続き

千行分くらいを書き直しているんだが、Invariantの構造にそって再帰を書いてっていう方法でいけそうなんですが、

場合分け12個あるうちの4個までかけた。残りがなぁ...

やりかた間違えているようなんだけど、まぁ、いいかな。いや、分量自体は増えるんですけど...

とにかくできることはわかってるので、やればよい

で、この Invariant の計算が両方向で成立することがわかると、insert だけでなく delete も書けるようになるらしい