diff --git a/.gitignore b/.gitignore
index bfb30ec..27329be 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /.lake
+.vscode
\ No newline at end of file
diff --git a/FormalTextbookModelTheory/ForMathlib/DLO.lean b/FormalTextbookModelTheory/ForMathlib/DLO.lean
index fb08c28..0b7a2e9 100644
--- a/FormalTextbookModelTheory/ForMathlib/DLO.lean
+++ b/FormalTextbookModelTheory/ForMathlib/DLO.lean
@@ -14,7 +14,7 @@ open Cardinal
 open FirstOrder Language Structure Theory Order
 open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂)
 
-namespace FirstOrder.Language.Order --region
+namespace FirstOrder.Language.Order
 
 section
 
@@ -243,4 +243,4 @@ theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.dlo := by
 
 end DLO --end
 
-end FirstOrder.Language.Order --end
+end FirstOrder.Language.Order
diff --git a/README.md b/README.md
index 4c48f19..dc33e7b 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,5 @@
-# FormalTextbookModelTheory
\ No newline at end of file
+# FormalTextbookModelTheory
+
+The end goal is to formalize the famous textbook Model Theory: An Introduction by David Marker.
+
+* Right know, the aleph0 categoricity of the theory of dense linear orders are proved. The essential part of the proof, which is the back-and-forth argument, was already in Mathlib but it was in terms of the instances LinearOrder, Countable etc. We just provided the dictionary to carry the proof to the language of model theory.
diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html
index ac32b62..2158c80 100644
--- a/blueprint/web/dep_graph_document.html
+++ b/blueprint/web/dep_graph_document.html
@@ -557,7 +557,7 @@ <h1 id="doc_title">Dependencies</h1>
     .width(width)
     .height(height)
     .fit(true)
-    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [label="\N",		penwidth=1.8	];	edge [arrowhead=vee];	"lem:realize-reflexivity"	[color=green,		fillcolor="#1CAC78",		label="realize-reflexivity",		shape=ellipse,		style=filled];	"def:preorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="preorder-dlo",		shape=box,		style=filled];	"lem:realize-reflexivity" -> "def:preorder-dlo"	[style=dashed];	"def:linearorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="linearorder-dlo",		shape=box,		style=filled];	"def:preorder-dlo" -> "def:linearorder-dlo"	[style=dashed];	"thm:dlo-aleph0-categorical"	[color=green,		fillcolor="#1CAC78",		label="dlo-aleph0-categorical",		shape=ellipse,		style=filled];	"def:linearorder-dlo" -> "thm:dlo-aleph0-categorical";	"lem:realize-total"	[color=green,		fillcolor="#1CAC78",		label="realize-total",		shape=ellipse,		style=filled];	"lem:realize-total" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-no-min"	[color=green,		fillcolor="#1CAC78",		label="realize-no-min",		shape=ellipse,		style=filled];	"lem:to-embedding"	[color=green,		fillcolor="#1CAC78",		label="to-embedding",		shape=ellipse,		style=filled];	"lem:to-isomorphism"	[color=green,		fillcolor="#1CAC78",		label="to-isomorphism",		shape=ellipse,		style=filled];	"lem:to-embedding" -> "lem:to-isomorphism";	"lem:to-isomorphism" -> "thm:dlo-aleph0-categorical";	"def:le-instance-language-order"	[color=green,		fillcolor="#B0ECA3",		label="le-instance-language-order",		shape=box,		style=filled];	"def:le-instance-language-order" -> "def:preorder-dlo"	[style=dashed];	"def:le-instance-language-order" -> "lem:to-embedding"	[style=dashed];	"lem:order-structure-of-le"	[color=green,		fillcolor="#1CAC78",		label="order-structure-of-le",		shape=ellipse,		style=filled];	"def:le-instance-language-order" -> "lem:order-structure-of-le"	[style=dashed];	"lem:vector-notation"	[color=green,		fillcolor="#1CAC78",		label="vector-notation",		shape=ellipse,		style=filled];	"lem:vector-notation" -> "lem:to-embedding";	"lem:vector-notation" -> "lem:order-structure-of-le";	"lem:vector-notation-under-composition"	[color=green,		fillcolor="#1CAC78",		label="vector-notation-under-composition",		shape=ellipse,		style=filled];	"lem:vector-notation-under-composition" -> "lem:to-embedding";	"lem:realize-transitivity"	[color=green,		fillcolor="#1CAC78",		label="realize-transitivity",		shape=ellipse,		style=filled];	"lem:realize-transitivity" -> "def:preorder-dlo"	[style=dashed];	"lem:realize-antisymmetric"	[color=green,		fillcolor="#1CAC78",		label="realize-antisymmetric",		shape=ellipse,		style=filled];	"lem:realize-antisymmetric" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-densely-ordered"	[color=green,		fillcolor="#1CAC78",		label="realize-densely-ordered",		shape=ellipse,		style=filled];	"lem:realize-no-max"	[color=green,		fillcolor="#1CAC78",		label="realize-no-max",		shape=ellipse,		style=filled];}`)
+    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [label="\N",		penwidth=1.8	];	edge [arrowhead=vee];	"lem:vector-notation"	[color=green,		fillcolor="#1CAC78",		label="vector-notation",		shape=ellipse,		style=filled];	"lem:order-structure-of-le"	[color=green,		fillcolor="#1CAC78",		label="order-structure-of-le",		shape=ellipse,		style=filled];	"lem:vector-notation" -> "lem:order-structure-of-le";	"lem:to-embedding"	[color=green,		fillcolor="#1CAC78",		label="to-embedding",		shape=ellipse,		style=filled];	"lem:vector-notation" -> "lem:to-embedding";	"lem:to-isomorphism"	[color=green,		fillcolor="#1CAC78",		label="to-isomorphism",		shape=ellipse,		style=filled];	"lem:to-embedding" -> "lem:to-isomorphism";	"thm:dlo-aleph0-categorical"	[color=green,		fillcolor="#1CAC78",		label="dlo-aleph0-categorical",		shape=ellipse,		style=filled];	"lem:to-isomorphism" -> "thm:dlo-aleph0-categorical";	"lem:realize-reflexivity"	[color=green,		fillcolor="#1CAC78",		label="realize-reflexivity",		shape=ellipse,		style=filled];	"def:preorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="preorder-dlo",		shape=box,		style=filled];	"lem:realize-reflexivity" -> "def:preorder-dlo"	[style=dashed];	"def:linearorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="linearorder-dlo",		shape=box,		style=filled];	"def:preorder-dlo" -> "def:linearorder-dlo"	[style=dashed];	"def:linearorder-dlo" -> "thm:dlo-aleph0-categorical";	"lem:realize-no-min"	[color=green,		fillcolor="#1CAC78",		label="realize-no-min",		shape=ellipse,		style=filled];	"def:le-instance-language-order"	[color=green,		fillcolor="#B0ECA3",		label="le-instance-language-order",		shape=box,		style=filled];	"def:le-instance-language-order" -> "lem:order-structure-of-le"	[style=dashed];	"def:le-instance-language-order" -> "lem:to-embedding"	[style=dashed];	"def:le-instance-language-order" -> "def:preorder-dlo"	[style=dashed];	"lem:vector-notation-under-composition"	[color=green,		fillcolor="#1CAC78",		label="vector-notation-under-composition",		shape=ellipse,		style=filled];	"lem:vector-notation-under-composition" -> "lem:to-embedding";	"lem:realize-transitivity"	[color=green,		fillcolor="#1CAC78",		label="realize-transitivity",		shape=ellipse,		style=filled];	"lem:realize-transitivity" -> "def:preorder-dlo"	[style=dashed];	"lem:realize-antisymmetric"	[color=green,		fillcolor="#1CAC78",		label="realize-antisymmetric",		shape=ellipse,		style=filled];	"lem:realize-antisymmetric" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-total"	[color=green,		fillcolor="#1CAC78",		label="realize-total",		shape=ellipse,		style=filled];	"lem:realize-total" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-densely-ordered"	[color=green,		fillcolor="#1CAC78",		label="realize-densely-ordered",		shape=ellipse,		style=filled];	"lem:realize-no-max"	[color=green,		fillcolor="#1CAC78",		label="realize-no-max",		shape=ellipse,		style=filled];}`)
     .on("end", interactive);
 
 latexLabelEscaper = function(label) {