change: align with mathlib

[iehality]

fix #537

To maintain compatibility with mathlib, import the entire Mathlib.

• Vorspiel
• Logic
• FirstOrder
• IntFO
• Propositional
• Modal
• ProvabilityLogic
• Meta
• Zoo

[iehality]

@SnO2WMaN

Modal 周辺の修正お願いします．

[SnO2WMaN]

Finset.boxが重複しており致命的な問題になっているので時間がかかるかもしれない．そもそも Finset.box という純粋に論理学的な演算をトップレベルで定義するのもあまり良くないと思っていて Finset.Logic.box みたいな名前にするべきだとは思っていたが．ただしこの場合 s.box (s : Finset) のような記述は出来ず，すごく煩雑になってしまう可能性はある．

[iehality]

Finset.boxが重複しており致命的な問題になっているので時間がかかるかもしれない．そもそも Finset.box という純粋に論理学的な演算をトップレベルで定義するのもあまり良くないと思っていて Finset.Logic.box みたいな名前にするべきだとは思っていたが．ただしこの場合 s.box (s : Finset) のような記述は出来ず，すごく煩雑になってしまう可能性はある．

instance [LO.Box α] : LO.Box (Finset α) を定義するのはどうだろうか．

[SnO2WMaN]

Finset.boxが重複しており致命的な問題になっているので時間がかかるかもしれない．そもそも Finset.box という純粋に論理学的な演算をトップレベルで定義するのもあまり良くないと思っていて Finset.Logic.box みたいな名前にするべきだとは思っていたが．ただしこの場合 s.box (s : Finset) のような記述は出来ず，すごく煩雑になってしまう可能性はある．

instance [LO.Box α] : LO.Box (Finset α) を定義するのはどうだろうか．

そもそも Finset.box や List.box をなぜか帰納的に定義していてよくわからなかったので別個立てて書き換えておく．