refactor(book): restructure chapters, extract Proof.lean, and fix the generated project

Bib.lean

@@ -104,6 +104,15 @@ def enderton2001 : Article where
   volume  := inlines!""
   number  := inlines!""
 
+def nederpelt2014 : Article where
+  title   := inlines!"Type Theory and Formal Proof: An Introduction"
+  authors := #[inlines!"Rob Nederpelt", inlines!"Herman Geuvers"]
+  journal := inlines!"Cambridge University Press, Cambridge"
+  year    := 2014
+  month   := none
+  volume  := inlines!""
+  number  := inlines!""
+
 def FAA2025 : Article where
   title   := inlines!"Formalizing Analysis of Algorithms, Autumn 2025"
   authors := #[inlines!"Sorrachai Yingchareonthawornchai"]

Book.lean

@@ -3,10 +3,10 @@ import Bib
 
 import CSwL.IntroCS
 import CSwL.IntroL
-import CSwL.Morphology
-import CSwL.Games
 import CSwL.Logic
 import CSwL.Sets
+import CSwL.SeaBattle
+import CSwL.Morphology
 import CSwL.InfEngine
 import CSwL.English
 
@@ -29,9 +29,9 @@ set_option verso.code.warnLineLength 80
 #doc (Manual) "Semântica computacional com Lean" =>
 {include CSwL.IntroCS}
 {include CSwL.IntroL}
-{include CSwL.Morphology}
-{include CSwL.Games}
 {include CSwL.Logic}
 {include CSwL.Sets}
+{include CSwL.SeaBattle}
+{include CSwL.Morphology}
 {include CSwL.InfEngine}
 {include CSwL.English}

CSwL/English.lean

@@ -46,32 +46,20 @@ A abreviações são como `def` mas são `unfold` automaticamente.
 
 ```lean
 abbrev Sentences := List Sentence
-```
 
-```lean (name := c2eval37)
 #eval Subject.Chomsky
-```
 
-```leanOutput c2eval37
-English.Subject.Chomsky
-```
-
-```lean (name := c2eval38)
 #eval Sentence.S Subject.Chomsky
   (Predicate.Wrote "Syntactic Structures")
 ```
 
-```leanOutput c2eval38
-English.Sentence.S (English.Subject.Chomsky) (English.Predicate.Wrote "Syntactic Structures")
-```
-
 A última saida acima lembra uma árvore, o que iremos chamar de _árvore
 sintática_.
 
-```
-         Sentence
-          /    \
-    Subject   Predicate
+```display
+ Sentence
+ |- Subject
+ |- Predicate
 ```
 
 O passo inverso é a _geração_, serializar uma estrutura que representa
@@ -82,19 +70,6 @@ instâncias para `ToString` de nossos tipos. Criar uma instância de uma
 classe é implementar os campos que a classe demanda e classes são
 `structure`. Algumas variações de sintaxe na declaração das instâncias.
 
-```lean (name := c2print7)
-#print ToString
-```
-
-```leanOutput c2print7
-class ToString.{u} (α : Type u) : Type u
-number of parameters: 1
-fields:
-  ToString.toString : α → String
-constructor:
-  ToString.mk.{u} {α : Type u} (toString : α → String) : ToString α
-```
-
 ```lean
 instance : ToString Subject where
   toString
@@ -121,10 +96,6 @@ def makeS (s : Subject) (p : Predicate) : Sentence := .S s p
   makeS .Chomsky (makeP "Syntactic Structures")
 ```
 
-```leanOutput c2eval39
-Chomsky wrote "Syntactic Structures"
-```
-
 
 ## Por que isso serve à semântica
 
@@ -201,15 +172,10 @@ E a sentença, com o sujeito no lugar.
 
 ```lean
 def dorothyLikesToto : t := likesToto dorothy
-```
 
-```lean (name := c3check12)
 #check dorothyLikesToto
 ```
 
-```leanOutput c3check12
-English.dorothyLikesToto : t
-```
 
 A derivação da sentença é uma sequência de duas aplicações, e cada
 passo é conferido pelos tipos. Uma combinação mal formada não chega a
@@ -299,6 +265,7 @@ entidade: `#check likes "Toto"` não compila, e o erro aponta o
 argumento — uma `String` onde se esperava um `e`. É a versão tipada de
 dizer que a combinação não é bem formada.
 
+
 # Um fragmento do inglês
 
 Em seguida, vamos implementar um fragmento um pouco mais realistico do inglês.  Ela é deliberadamente básica e grosseira, queremos capturar a sintaxe de sentenças como:
@@ -789,7 +756,6 @@ O problema é que `rcn4`/`rcn5` não são recursivas: cada uma coordena exatamen
 ::::
 
 
-
 ```lean
 end English
 ```