SnO₂WMaN

See R.Goldblatt, "Logic of Time and Computation" p.36.

Completeness (Canonicity) of `KTMk` is based on this fact. See R. Goldblatt, "Logics of Time and Computation", Chapter 7 (pp,48-50).

Prove `𝐈𝚺₁` is Δ_1 definable

1

現状では算術的完全性を経由して様相論理`S`の純粋な様相論理的な性質を証明しているのでこれ以降すべての証明が`sorryAx`に依存してしまう https://github.com/FormalizedFormalLogic/Foundation/blob/5d0eb4e51de098b32e1623f00fe8c84dff24a004/Foundation/ProvabilityLogic/Basic.lean#L18

related #347

Remove `List.conj₂` and `List.disj₂`

1

少なくとも様相論理と命題論理でEntailmentのContextとして陽としてリストを使うのをやめてコードを簡略化することに成功しており，おそらく`List.disj`および`List.conj`で議論は事足りるようになるはず．2つあるももただ物事を複雑にするだけなので，いずれ削除する．

### Font Name JuliaMono ### Link to font source - https://juliamono.netlify.app/ - https://github.com/cormullion/juliamono ### Link to font license https://github.com/cormullion/juliamono/blob/master/LICENSE ### Additional context _No response_

feat: Add `Book` for bibliography

3

related #436

There are few bibliograpy type in now `Article`, `Thesis`, `ArXiv`, `InProceedings` in Verso Manual, however it is useful (or necessary) for adding more types e.g. `Book`, `Web` or else.

### Describe the bug Currently, downloading link "Shippori Mincho B1" is not working: https://api.fontsource.org/v1/download/shippori-mincho-b1 I don't know some other fonts are same situation, but similar series of font "Shippori Antique...