SnO₂WMaN
SnO₂WMaN
`Consistent 𝓢 → 𝓢 ⊬ ⊥` となっているものを `[Consistent 𝓢] → 𝓢 ⊬ ⊥` にして `simp` を使えるようにしたほうが便利だと思う．
close #409
現状出来ている以上，算術的完全性を示すには別にフレームがrootedかつantisymmetric, transのみはずでよいのだが，この条件をまとめたものをtreeというのは完全に嘘なので（ダイヤモンド形のフレームはこれを満たし，これは普通木とは呼ばないはず）命名を変える．あるいは，少なくともTreeUnravellingしたフレームは実際に木になるので，IsTreeの定義を改める（2項関係が木を成している，という定義の形式的な記述をどうすればよいかは実は自分はよくわかっていない，他の文献もあまりきちんとは書いてない．）
なぜか忘れていたが`box`, `dia`を`L`, `M`に書き換える