refactor(Modal): Commonize Kripke Semantics Part.2

[SnO2WMaN]

trafficstars

相当に時間がかかりそうなのでのんびりとしたペースで行う．

[iehality]

abbrev FrameClassOfSystem (α : Type u) {S : Type u} [System (Formula α) S] (𝓢 : S) : FrameClass.Dep α := { (F : Frame.Dep α) | F ⊧* System.theory 𝓢 }

前回指摘しておくべきことだったが，FrameClassOfSystem の α と S のuniverse level をそろえる意味はないと思うのでType*で書くべきだと思う．

[SnO2WMaN]

#124 が終わり次第．