fix & refactor

Arithmetization.lean

@@ -24,7 +24,6 @@ import Arithmetization.ISigmaOne.Bit
 import Arithmetization.ISigmaOne.HFS.Basic
 import Arithmetization.ISigmaOne.HFS.Seq
 import Arithmetization.ISigmaOne.HFS.PRF
-import Arithmetization.ISigmaOne.HFS.Supplemental
 import Arithmetization.ISigmaOne.HFS.Fixpoint
 
 import Arithmetization.ISigmaOne.Metamath.Term.Basic
@@ -47,4 +46,5 @@ import Arithmetization.Incompleteness.Theory
 import Arithmetization.Incompleteness.FormalizedArithmetic
 import Arithmetization.Incompleteness.D1
 import Arithmetization.Incompleteness.D3
+import Arithmetization.Incompleteness.First
 import Arithmetization.Incompleteness.Second

Arithmetization/ISigmaOne/Metamath.lean

@@ -1,10 +1,15 @@
-import Arithmetization.ISigmaOne.Metamath.DerivabilityConditions.D1
-import Arithmetization.ISigmaOne.Metamath.DerivabilityConditions.D3
+import Arithmetization.ISigmaOne.Metamath.Term.Basic
+import Arithmetization.ISigmaOne.Metamath.Term.Functions
+import Arithmetization.ISigmaOne.Metamath.Term.Typed
 
-namespace LO.FirstOrder.Arith
+import Arithmetization.ISigmaOne.Metamath.Formula.Basic
+import Arithmetization.ISigmaOne.Metamath.Formula.Functions
+import Arithmetization.ISigmaOne.Metamath.Formula.Iteration
+import Arithmetization.ISigmaOne.Metamath.Formula.Typed
 
-variable (T : Theory ℒₒᵣ)
+import Arithmetization.ISigmaOne.Metamath.Proof.Thy
+import Arithmetization.ISigmaOne.Metamath.Proof.Derivation
+import Arithmetization.ISigmaOne.Metamath.Proof.Typed
 
-
-
-end LO.FirstOrder.Arith
+import Arithmetization.ISigmaOne.Metamath.Coding
+import Arithmetization.ISigmaOne.Metamath.CodedTheory

Arithmetization/Incompleteness/FormalizedArithmetic.lean

@@ -1,4 +1,4 @@
-import Arithmetization.ISigmaOne.Metamath.Proof.Typed
+import Arithmetization.ISigmaOne.Metamath
 
 /-!
 

Arithmetization/Incompleteness/Theory.lean

@@ -1,4 +1,3 @@
-import Arithmetization.ISigmaOne.Metamath.CodedTheory
 import Arithmetization.Incompleteness.FormalizedArithmetic
 
 /-!