diff --git a/ConNF.lean b/ConNF.lean
index da084e0f6e..c5dd60ef23 100644
--- a/ConNF.lean
+++ b/ConNF.lean
@@ -8,25 +8,13 @@ import ConNF.Basic.Set
 import ConNF.Basic.Transfer
 import ConNF.Basic.WellOrder
 import ConNF.Construction.Code
-import ConNF.Construction.ConstructHypothesis
-import ConNF.Construction.ConstructMotive
-import ConNF.Construction.Externalise
-import ConNF.Construction.Hailperin
-import ConNF.Construction.InductionStatement
 import ConNF.Construction.NewModelData
-import ConNF.Construction.RaiseStrong
-import ConNF.Construction.Result
-import ConNF.Construction.RunInduction
-import ConNF.Construction.TTT
 import ConNF.Counting.BaseCoding
 import ConNF.Counting.BaseCounting
 import ConNF.Counting.CodingFunction
 import ConNF.Counting.Conclusions
 import ConNF.Counting.CountSupportOrbit
 import ConNF.Counting.Recode
-import ConNF.Counting.SMulSpec
-import ConNF.Counting.Spec
-import ConNF.Counting.SpecSame
 import ConNF.Counting.Strong
 import ConNF.Counting.Twist
 import ConNF.FOA.BaseAction
@@ -38,6 +26,15 @@ import ConNF.FOA.StrAction
 import ConNF.FOA.StrActionFOA
 import ConNF.FOA.StrApprox
 import ConNF.FOA.StrApproxFOA
+import ConNF.Model.ConstructHypothesis
+import ConNF.Model.ConstructMotive
+import ConNF.Model.Externalise
+import ConNF.Model.Hailperin
+import ConNF.Model.InductionStatement
+import ConNF.Model.RaiseStrong
+import ConNF.Model.Result
+import ConNF.Model.RunInduction
+import ConNF.Model.TTT
 import ConNF.Setup.Atom
 import ConNF.Setup.BasePerm
 import ConNF.Setup.BasePositions
@@ -59,3 +56,6 @@ import ConNF.Setup.StrSet
 import ConNF.Setup.Support
 import ConNF.Setup.Tree
 import ConNF.Setup.TypeIndex
+import ConNF.Strong.SMulSpec
+import ConNF.Strong.Spec
+import ConNF.Strong.SpecSame
diff --git a/ConNF/Counting/BaseCoding.lean b/ConNF/Counting/BaseCoding.lean
index 66306aa03e..3173bc02fa 100644
--- a/ConNF/Counting/BaseCoding.lean
+++ b/ConNF/Counting/BaseCoding.lean
@@ -1,4 +1,4 @@
-import ConNF.Counting.SpecSame
+import ConNF.Strong.SpecSame
 
 /-!
 # Coding the base type
diff --git a/ConNF/Counting/CountSupportOrbit.lean b/ConNF/Counting/CountSupportOrbit.lean
index e785cfb99b..623e73b4a3 100644
--- a/ConNF/Counting/CountSupportOrbit.lean
+++ b/ConNF/Counting/CountSupportOrbit.lean
@@ -1,5 +1,5 @@
-import ConNF.Counting.SMulSpec
-import ConNF.Counting.SpecSame
+import ConNF.Strong.SMulSpec
+import ConNF.Strong.SpecSame
 
 /-!
 # Counting support orbits
diff --git a/ConNF/Construction/ConstructHypothesis.lean b/ConNF/Model/ConstructHypothesis.lean
similarity index 99%
rename from ConNF/Construction/ConstructHypothesis.lean
rename to ConNF/Model/ConstructHypothesis.lean
index dfa55c62b6..1addd8e887 100644
--- a/ConNF/Construction/ConstructHypothesis.lean
+++ b/ConNF/Model/ConstructHypothesis.lean
@@ -1,4 +1,4 @@
-import ConNF.Construction.ConstructMotive
+import ConNF.Model.ConstructMotive
 
 /-!
 # New file
diff --git a/ConNF/Construction/ConstructMotive.lean b/ConNF/Model/ConstructMotive.lean
similarity index 99%
rename from ConNF/Construction/ConstructMotive.lean
rename to ConNF/Model/ConstructMotive.lean
index 2ace2ba796..1d879fe81a 100644
--- a/ConNF/Construction/ConstructMotive.lean
+++ b/ConNF/Model/ConstructMotive.lean
@@ -1,4 +1,4 @@
-import ConNF.Construction.InductionStatement
+import ConNF.Model.InductionStatement
 import ConNF.Construction.NewModelData
 import ConNF.Counting.Conclusions
 
diff --git a/ConNF/Construction/Externalise.lean b/ConNF/Model/Externalise.lean
similarity index 99%
rename from ConNF/Construction/Externalise.lean
rename to ConNF/Model/Externalise.lean
index 758dfd96b3..1501cbf228 100644
--- a/ConNF/Construction/Externalise.lean
+++ b/ConNF/Model/Externalise.lean
@@ -1,4 +1,4 @@
-import ConNF.Construction.RunInduction
+import ConNF.Model.RunInduction
 
 /-!
 # Externalisation
diff --git a/ConNF/Construction/Hailperin.lean b/ConNF/Model/Hailperin.lean
similarity index 99%
rename from ConNF/Construction/Hailperin.lean
rename to ConNF/Model/Hailperin.lean
index 1fc40153db..eb0f125a3f 100644
--- a/ConNF/Construction/Hailperin.lean
+++ b/ConNF/Model/Hailperin.lean
@@ -1,4 +1,4 @@
-import ConNF.Construction.TTT
+import ConNF.Model.TTT
 
 /-!
 # New file
diff --git a/ConNF/Construction/InductionStatement.lean b/ConNF/Model/InductionStatement.lean
similarity index 100%
rename from ConNF/Construction/InductionStatement.lean
rename to ConNF/Model/InductionStatement.lean
diff --git a/ConNF/Construction/RaiseStrong.lean b/ConNF/Model/RaiseStrong.lean
similarity index 99%
rename from ConNF/Construction/RaiseStrong.lean
rename to ConNF/Model/RaiseStrong.lean
index 7187712268..b1aa861eb7 100644
--- a/ConNF/Construction/RaiseStrong.lean
+++ b/ConNF/Model/RaiseStrong.lean
@@ -1,4 +1,4 @@
-import ConNF.Construction.Externalise
+import ConNF.Model.Externalise
 
 /-!
 # New file
diff --git a/ConNF/Construction/Result.lean b/ConNF/Model/Result.lean
similarity index 98%
rename from ConNF/Construction/Result.lean
rename to ConNF/Model/Result.lean
index 11a38b311d..db9c168ba2 100644
--- a/ConNF/Construction/Result.lean
+++ b/ConNF/Model/Result.lean
@@ -1,4 +1,4 @@
-import ConNF.Construction.Hailperin
+import ConNF.Model.Hailperin
 
 /-!
 # New file
diff --git a/ConNF/Construction/RunInduction.lean b/ConNF/Model/RunInduction.lean
similarity index 94%
rename from ConNF/Construction/RunInduction.lean
rename to ConNF/Model/RunInduction.lean
index c8bc85395f..d3e9fae505 100644
--- a/ConNF/Construction/RunInduction.lean
+++ b/ConNF/Model/RunInduction.lean
@@ -1,5 +1,5 @@
 import ConNF.Basic.InductiveConstruction
-import ConNF.Construction.ConstructHypothesis
+import ConNF.Model.ConstructHypothesis
 
 /-!
 # New file
diff --git a/ConNF/Construction/TTT.lean b/ConNF/Model/TTT.lean
similarity index 99%
rename from ConNF/Construction/TTT.lean
rename to ConNF/Model/TTT.lean
index 09138dc0ba..18f318985a 100644
--- a/ConNF/Construction/TTT.lean
+++ b/ConNF/Model/TTT.lean
@@ -1,4 +1,4 @@
-import ConNF.Construction.RaiseStrong
+import ConNF.Model.RaiseStrong
 
 /-!
 # New file
diff --git a/ConNF/Counting/SMulSpec.lean b/ConNF/Strong/SMulSpec.lean
similarity index 99%
rename from ConNF/Counting/SMulSpec.lean
rename to ConNF/Strong/SMulSpec.lean
index 55a4c76967..494d72fe00 100644
--- a/ConNF/Counting/SMulSpec.lean
+++ b/ConNF/Strong/SMulSpec.lean
@@ -1,4 +1,4 @@
-import ConNF.Counting.Spec
+import ConNF.Strong.Spec
 
 /-!
 # Action on specifications
diff --git a/ConNF/Counting/Spec.lean b/ConNF/Strong/Spec.lean
similarity index 100%
rename from ConNF/Counting/Spec.lean
rename to ConNF/Strong/Spec.lean
diff --git a/ConNF/Counting/SpecSame.lean b/ConNF/Strong/SpecSame.lean
similarity index 99%
rename from ConNF/Counting/SpecSame.lean
rename to ConNF/Strong/SpecSame.lean
index 8bbebdecbf..2480e07574 100644
--- a/ConNF/Counting/SpecSame.lean
+++ b/ConNF/Strong/SpecSame.lean
@@ -1,6 +1,6 @@
 import ConNF.FOA.StrActionFOA
 import ConNF.Counting.Strong
-import ConNF.Counting.Spec
+import ConNF.Strong.Spec
 
 /-!
 # Supports with the same specification
diff --git a/DependencyGraph.lean b/DependencyGraph.lean
index 35dcfd19c7..15e1a42480 100644
--- a/DependencyGraph.lean
+++ b/DependencyGraph.lean
@@ -43,7 +43,7 @@ elab "#deptree " : command => do
   for (gp, _) in groups imports do
     h.write ("subgraph cluster_" ++ nameCode gp ++ " {\n").toUTF8
     for (k, v) in imports do
-      if (`ConNF).isPrefixOf k && group k = gp then do
+      if (`ConNF).isPrefixOf k && k != `ConNF && group k = gp then do
         printDeps₁ k v (fun s => h.write s.toUTF8)
     h.write ("label = \"" ++ gp.toString ++ "\";\n").toUTF8
     h.write ("margin = 32;\n").toUTF8
@@ -52,7 +52,7 @@ elab "#deptree " : command => do
     h.write ("color = cyan4;\n").toUTF8
     h.write "}\n".toUTF8
   for (k, v) in imports do
-    if (`ConNF).isPrefixOf k then do
+    if (`ConNF).isPrefixOf k && k != `ConNF then do
       printDeps₂ k v (fun s => h.write s.toUTF8)
   h.write "}\n".toUTF8
 
@@ -77,10 +77,10 @@ def allFiles (env : Environment) : List Name :=
     (toString · < toString ·)
 
 def allDecls (env : Environment) : Elab.Command.CommandElabM NameSet :=
-  (fun l => RBTree.ofList (l.map (fun a => a.toList)).join) <$>
+  (fun l => RBTree.ofList (l.map (fun a => a.toList)).flatten) <$>
     (mapM allDeclsIn (allFiles env))
 
-/-- `#index` computes an index of the declations in the project and saves it to `index.csv`. -/
+/-- `#index` computes an index of the declarations in the project and saves it to `index.csv`. -/
 elab "#index " : command => do
   let env ← getEnv
   let allDecls ← allDecls env