diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
new file mode 100644
index 00000000..66035eaf
--- /dev/null
+++ b/.devcontainer/Dockerfile
@@ -0,0 +1,9 @@
+FROM mcr.microsoft.com/devcontainers/base:jammy
+
+USER vscode
+WORKDIR /home/vscode
+ENV HOME=/home/vscode
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+ENV PATH="/home/vscode/.elan/bin:${PATH}"
\ No newline at end of file
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
new file mode 100644
index 00000000..90dff8dd
--- /dev/null
+++ b/.devcontainer/devcontainer.json
@@ -0,0 +1,21 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the
+// README at: https://github.com/devcontainers/templates/tree/main/src/ubuntu
+{
+  "name": "Lean DevContainer on Ubuntu",
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
+
+  "onCreateCommand": "lake exe cache get! && lake build",
+
+  "postStartCommand": "git config --global --add safe.directory ${containerWorkspaceFolder}",
+
+  "customizations": {
+    "vscode" : {
+      "extensions" : [
+        "leanprover.lean4",
+        "mhutchie.git-graph"
+      ]
+    }
+  }
+}
\ No newline at end of file
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 903ce5d9..be042a44 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -26,21 +26,15 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  build: 
+  build:
     runs-on: ubuntu-latest
     steps:
-      - name: Install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - name: Checkout
-        uses: actions/checkout@v3
-      - name: Download cached build
-        run: lake exe cache get
-      - name: Build SciLean
-        run: lake build
+      - name: checkout
+        uses: actions/checkout@v4
+      - name: lean action
+        uses: leanprover/lean-action@v1
+        with:
+          build-args: "--log-level=error"
       - name: Run Tests
         run: make test
       - name: Run Examples
diff --git a/SciLean/Data/FinProd.lean b/SciLean/Data/FinProd.lean
new file mode 100644
index 00000000..aef29f26
--- /dev/null
+++ b/SciLean/Data/FinProd.lean
@@ -0,0 +1,61 @@
+import SciLean.Data.IndexType
+
+namespace SciLean
+
+/-- Give `Fin n₁ × ... × Fin nₘ` for a list `[n₁,..., nₘ]`  -/
+def FinProd : List Nat → Type
+  | [] => Unit
+  | [n] => Fin n
+  | n :: (m :: ns) => Fin n × FinProd (m :: ns)
+
+instance instIndexTypeFinProd (l : List Nat) : IndexType (FinProd l) :=
+  match l with
+  | []  => by simp[FinProd]; infer_instance
+  | [n] => by simp[FinProd]; infer_instance
+  | n :: m :: ns =>
+    have e := instIndexTypeFinProd (m :: ns)
+    by simp[FinProd]; infer_instance
+
+instance instToStringFinProd (l : List Nat) : ToString (FinProd l) :=
+  match l with
+  | []  => by simp[FinProd]; infer_instance
+  | [n] => by simp[FinProd]; infer_instance
+  | n :: m :: ns =>
+    have e := instToStringFinProd (m :: ns)
+    by simp[FinProd]; infer_instance
+
+/-- Given `(i₁, ..., iₘ) : Fin n₁ × ... × Fin nₘ` return `[i₁.1,..., iₘ.1]` -/
+def FinProd.toList {l} (is : FinProd l) : List Nat :=
+  match l, is with
+  | [], _ => []
+  | [_], i => [i.1]
+  | _ :: _ :: _, (i, is) => i :: is.toList
+
+/-- Given `(i₁, ..., iₘ) : Fin n₁ × ... × Fin nₘ` return `[n₁-i₁.1-1,..., nₘ-iₘ.1-1]` -/
+def FinProd.toListComplement {l} (is : FinProd l) : List Nat :=
+  match l, is with
+  | [], _ => []
+  | [n], i => [n-i.1-1]
+  | n :: _ :: _, (i, is) => (n-i.1-1) :: is.toListComplement
+
+
+-- #eval show IO Unit from do
+--   let l := [2,3,4]
+--   let N := size (FinProd l)
+--   for i in fullRange (Fin N) do
+--     let x : FinProd l := IndexType.fromFin i
+--     IO.println s!"{x}"
+
+--   IO.println "hoho"
+
+--   for i in fullRange (FinProd [2,3]) do
+--     IO.println s!"{i}"
+
+--   IO.println "hihi"
+
+
+--- tests
+example : FinProd [] = Unit := by rfl
+example (n) : FinProd [n] = (Fin n) := by rfl
+example (n m) : FinProd [n,m] = (Fin n × Fin m) := by rfl
+example : FinProd [1,2,4] = (Fin 1 × Fin 2 × Fin 4) := by rfl
diff --git a/SciLean/Data/IndexType.lean b/SciLean/Data/IndexType.lean
index a5e63902..f46847ad 100644
--- a/SciLean/Data/IndexType.lean
+++ b/SciLean/Data/IndexType.lean
@@ -5,6 +5,8 @@ import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Sum
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Algebra.Order.GroupWithZero.Canonical
+import Mathlib.Tactic.ProxyType
+import Mathlib.Tactic.DeriveFintype
 
 import SciLean.Util.SorryProof
 import SciLean.Tactic.RefinedSimp
@@ -27,6 +29,30 @@ instance (a : List α) : Size a where
 
 inductive IndexType.Range (I : Type u)
   | full
+  -- endpoint
+  -- startpoint
+  -- interval
+
+@[inline]
+def IndexType.Range.ofEquiv (_ : I ≃ J) (i : Range I) : Range J :=
+  match i with
+  | .full => .full
+
+@[inline]
+def IndexType.Range.ofProd (i : Range (I×J)) : Range I × Range J :=
+  match i with
+  | .full => (.full, .full)
+
+@[inline]
+def IndexType.Range.prod (i : Range I) (j : Range J) : Range (I×J) :=
+  match i, j with
+  | .full, .full => .full
+
+@[inline]
+def IndexType.Range.ofSigma (i : Range ((_:I)×J)) : Range I × Range J :=
+  match i with
+  | .full => (.full, .full)
+
 
 inductive IndexType.Stream (I : Type u) where
   /-- Stream for range `range` that has not been started -/
@@ -36,6 +62,48 @@ inductive IndexType.Stream (I : Type u) where
   -- /-- Stream that has been exhausted -/
   -- | done
 
+@[inline]
+def IndexType.Stream.val! [Inhabited I] (s : Stream I) : I :=
+  match s with
+  | .start _ => panic! "can't take value of start stream!"
+  | .val i _ => i
+
+@[inline]
+def IndexType.Stream.ofEquiv (f : I ≃ J) (i : Stream I) : Stream J :=
+  match i with
+  | .start r => .start (r.ofEquiv f)
+  | .val i r => .val (f i) (r.ofEquiv f)
+
+@[inline]
+def IndexType.Stream.ofProd (i : Stream (I×J)) : Stream I × Stream J :=
+  match i with
+  | .start r =>
+    let (r,s) := r.ofProd
+    (.start r, .start s)
+  | .val (i,j) r =>
+    let (r, s) := r.ofProd
+    (.val i r, .val j s)
+
+@[inline]
+def IndexType.Stream.prod (i : Stream I) (j : Stream J) : Stream (I×J) :=
+  match i, j with
+  | .start ri, .start rj => .start (ri.prod rj)
+  | .start ri, .val _ rj => .start (ri.prod rj)
+  | .val _ ri, .start rj => .start (ri.prod rj)
+  | .val i ri, .val j rj => .val (i,j) (ri.prod rj)
+
+
+@[inline]
+def IndexType.Stream.ofSigma (i : Stream ((_:I)×J)) : Stream I × Stream J :=
+  match i with
+  | .start r =>
+    let (r,s) := r.ofSigma
+    (.start r, .start s)
+  | .val ⟨i,j⟩ r =>
+    let (r, s) := r.ofSigma
+    (.val i r, .val j s)
+
+
 -- This is alternative to LeanColls.IndexType which unfortunatelly has two universe parameters
 -- and because of that it is very difficult to work with.
 class IndexType (I : Type u) extends Fintype I, Stream (IndexType.Stream I) I, Size I where
@@ -50,7 +118,13 @@ def IndexType.first? (I : Type u) [IndexType I] : Option I :=
   else
     .none
 
-
+def IndexType.Range.first? {I : Type u} [IndexType I] (r : Range I) : Option I :=
+  match r with
+  | .full =>
+    if h : size I ≠ 0 then
+      .some (IndexType.fromFin ⟨0, by omega⟩)
+    else
+      .none
 
 
 instance : IndexType Empty where
@@ -65,6 +139,18 @@ instance : IndexType Unit where
   fromFin _ := ()
   next? _ := .none
 
+instance : IndexType Bool where
+  size := 2
+  toFin x := match x with | false => 0 | true => 1
+  fromFin x := match x with | ⟨0,_⟩ => false | ⟨1,_⟩ => true
+  next? s :=
+    match s with
+    | .start r => .some (false, .val false r)
+    | .val val r =>
+      match val with
+      | false => .some (true, .val true r)
+      | true => .none
+
 instance : IndexType (Fin n) where
   size := n
   toFin x := x
@@ -93,23 +179,70 @@ instance {α β} [IndexType α] [IndexType β] : IndexType (α × β) where
     let i : Fin (size α) := ⟨ij.1 % size α, by sorry_proof⟩
     let j : Fin (size β) := ⟨ij.1 / size α, by sorry_proof⟩
     (IndexType.fromFin i, IndexType.fromFin j)
+  next? s :=
+    match s with
+    | .start r =>
+      let (ri, rj) := r.ofProd
+      match ri.first?, rj.first? with
+      | .some i, .some j => .some ((i,j), .val (i,j) r)
+      | _, _ => .none
+    | .val (i,j) r =>
+      let (ri,rj) := r.ofProd
+      let si := IndexType.Stream.val i ri
+      let sj := IndexType.Stream.val j rj
+      match Stream.next? si with
+      | .some (i', si) => .some ((i',j), si.prod sj)
+      | .none =>
+        match ri.first?, Stream.next? sj with
+        | .some i', .some (j', sj) => .some ((i',j'), (IndexType.Stream.val i' ri).prod sj)
+        | _, _ => .none
+    -- match s with
+    -- | .start _r =>
+    --   if let .some a := IndexType.first? α then
+    --     if let .some b := IndexType.first? β then
+    --       .some (⟨a,b⟩, .val ⟨a,b⟩ .full) -- todo: split the range somehow
+    --     else
+    --       .none
+    --   else
+    --     .none
+    -- | .val ⟨a,b⟩ _r =>
+    --   if let .some sa := Stream.next? (IndexType.Stream.val a .full) then
+    --     .some (⟨sa.1,b⟩, .val ⟨sa.1,b⟩ .full)
+    --   else
+    --     if let .some sb := Stream.next? (IndexType.Stream.val b .full) then
+    --       if let .some a := IndexType.first? α then
+    --         .some (⟨a,sb.1⟩, .val ⟨a,sb.1⟩ .full)
+    --       else
+    --         .none
+    --     else
+    --       .none
+
+
+instance {α β} [IndexType α] [IndexType β] : IndexType ((_ : α) × β) where
+  size := size α * size β
+  toFin := fun ⟨a,b⟩ => ⟨(IndexType.toFin a).1 + size α * (IndexType.toFin b).1, by sorry_proof⟩
+  fromFin ij :=
+    -- this choice will result in column major matrices
+    let i : Fin (size α) := ⟨ij.1 % size α, by sorry_proof⟩
+    let j : Fin (size β) := ⟨ij.1 / size α, by sorry_proof⟩
+    ⟨IndexType.fromFin i, IndexType.fromFin j⟩
   next? s :=
     match s with
     | .start _r =>
       if let .some a := IndexType.first? α then
         if let .some b := IndexType.first? β then
-          .some ((a,b), .val (a,b) .full) -- todo: split the range somehow
+          .some (⟨a,b⟩, .val ⟨a,b⟩ .full) -- todo: split the range somehow
         else
           .none
       else
         .none
-    | .val (a,b) _r =>
+    | .val ⟨a,b⟩ _r =>
       if let .some sa := Stream.next? (IndexType.Stream.val a .full) then
-        .some ((sa.1,b), .val (sa.1,b) .full)
+        .some (⟨sa.1,b⟩, .val ⟨sa.1,b⟩ .full)
       else
         if let .some sb := Stream.next? (IndexType.Stream.val b .full) then
           if let .some a := IndexType.first? α then
-            .some ((a,sb.1), .val (a,sb.1) .full)
+            .some (⟨a,sb.1⟩, .val ⟨a,sb.1⟩ .full)
           else
             .none
         else
@@ -183,6 +316,33 @@ instance (a b : Int) : IndexType (Icc a b) where
         .none
 
 
+def IndexType.ofEquiv [IndexType I] [Fintype J] (f : I≃J) : IndexType J where
+  size := size I
+  toFin j := toFin (f.symm j)
+  fromFin idx := f (fromFin idx)
+  next? s :=
+    match Stream.next? (s.ofEquiv f.symm) with
+    | .some (i, si) => .some (f i, si.ofEquiv f)
+    | .none => .none
+
+
+open Lean Elab Command
+def mkIndexTypeInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  if declNames.size != 1 then
+    return false -- mutually inductive types are not supported
+  let id : Ident := mkIdent declNames[0]!
+  try
+    elabCommand (← `(deriving instance Fintype for $id))
+  catch _ =>
+    pure ()
+
+  elabCommand (← `(instance : IndexType $id := IndexType.ofEquiv (proxy_equiv% $id)))
+  return true
+
+initialize
+  registerDerivingHandler ``IndexType mkIndexTypeInstanceHandler
+
+
 namespace SciLean
 end SciLean
 
@@ -311,13 +471,13 @@ theorem reduce_linearize {I X : Type _} [IndexType I] (init : X) (f : I → X) (
 
 
 @[sum_push]
-theorem sum_pair {I X : Type _} [Add X] [Zero X] [IndexType I]
-    (f g : I → X) :
+theorem sum_pair {I X : Type _} [Add X] [Zero X] [Add Y] [Zero Y] [IndexType I]
+    (f : I → X) (g : I → Y) :
     ∑ i, (f i, g i) = (∑ i, f i, ∑ i, g i) := sorry_proof
 
 @[sum_pull]
-theorem pair_sum {I X : Type _} [Add X] [Zero X] [IndexType I]
-    (f g : I → X) :
+theorem pair_sum {I X : Type _} [Add X] [Zero X] [Add Y] [Zero Y] [IndexType I]
+    (f : I → X) (g : I → Y) :
     (∑ i, f i, ∑ i, g i) = ∑ i, (f i, g i) := sorry_proof
 
 
diff --git a/SciLean/Tactic/GTrans/MetaLCtxM.lean b/SciLean/Tactic/GTrans/MetaLCtxM.lean
index f0c9a661..0599e117 100644
--- a/SciLean/Tactic/GTrans/MetaLCtxM.lean
+++ b/SciLean/Tactic/GTrans/MetaLCtxM.lean
@@ -38,6 +38,29 @@ def _root_.Lean.Meta.Context.mkCtxCfg (ctx : ContextCtx) (cfg : ContextCfg) : Me
 
 -- TODO: change the monad such that we can only add variables to the context and not remove them
 --       or completely changes the context
+/-- Similar to `MetaM` but allows modifying local context.
+
+Most imporantly it has a variant of `lambdaTelescope` called `introLet` such that instead of
+```
+lambdaTelescope e fun xs b => do
+  f xs b
+```
+we can call
+```
+let (b,xs) ← lambdaIntro e
+f xs b
+```
+
+For example running `lambdaTelescope` does not work well with for loops but `lambdaIntro` does.
+
+Important functions introducing new free variables to the context:
+  - `lambdaIntro`
+  - `letIntro`
+  - `introLocalDecl`
+  - `introLetDecl`
+
+Also you can run `MetaLCtxM` inside of `MetaM` with `MetaLCtxM.runInMeta`.
+ -/
 abbrev MetaLCtxM  := ReaderT Meta.ContextCfg $ StateT Meta.ContextCtx $ StateRefT Meta.State CoreM
 
 
diff --git a/SciLean/Tactic/LSimp/Types.lean b/SciLean/Tactic/LSimp/Types.lean
index e866bd9a..a055c1fc 100644
--- a/SciLean/Tactic/LSimp/Types.lean
+++ b/SciLean/Tactic/LSimp/Types.lean
@@ -20,9 +20,21 @@ namespace SciLean.Tactic.LSimp
 -- Result ------------------------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------------
 
+
+/-- Result of `lsimp` -/
 structure Result where
+  /-- Result of simplification  -/
   expr : Expr
+  /-- Proof that the result is propositionally equal to the original expression. It is `none` if
+  it is defeq to the original. -/
   proof? : Option Expr := none
+  /-- This array keeps track of the newly introduced free variables that appear in the result.
+  We run `lsimp` in `MetaLCtxM` which allows modifying the local context by adding new free
+  variables.
+
+  See `Result.bindVars` which is a function that takes the result and the proof and binds all
+  these newly introduced free variables such that the result is valid in the original context
+  of the expression we are simplifying. -/
   vars : Array Expr := #[]
   cache          : Bool := true
   deriving Inhabited
diff --git a/notes.org b/notes.org
index 64cb3812..4ea2637a 100644
--- a/notes.org
+++ b/notes.org
@@ -21,7 +21,7 @@
 *** TODO Lean Framework
 
    Implement these to in the order to get these examples working:
-     1. Harmonic Oscilator
+     1. Harmonic Oscillator
      2. Pendulum
      3. NBody
      4. NPendulum in 2D
diff --git a/test/ScientificComputingInLean/tensor_operations.lean b/test/ScientificComputingInLean/tensor_operations.lean
index 692cea08..701bf6ef 100644
--- a/test/ScientificComputingInLean/tensor_operations.lean
+++ b/test/ScientificComputingInLean/tensor_operations.lean
@@ -1,5 +1,6 @@
 import SciLean
 import SciLean.Tactic.InferVar
+import Mathlib.Tactic.ProxyType
 
 open SciLean Scalar
 
@@ -10,7 +11,7 @@ open SciLean Scalar
 
 def map {I : Type} [IndexType I] (x : Float^[I]) (f : Float → Float) := Id.run do
   let mut x' := x
-  for i in IndexType.univ I do
+  for i in fullRange I do
     x'[i] := f x'[i]
   return x'
 
@@ -19,29 +20,29 @@ def map {I : Type} [IndexType I] (x : Float^[I]) (f : Float → Float) := Id.run
 #guard_msgs in
 #eval ⊞[1.0,2.0,3.0].mapMono (fun x => sqrt x)
 
-/-- info: ⊞[1.000000, 1.414214, 1.732051, 2.000000] -/
+/-- info: ⊞[1.000000, 1.732051, 1.414214, 2.000000] -/
 #guard_msgs in
 #eval ⊞[1.0,2.0;3.0,4.0].mapMono (fun x => sqrt x)
 
 /-- info: ⊞[0.000000, 1.000000, 1.414214, 1.732051, 2.000000, 2.236068, 2.449490, 2.645751] -/
 #guard_msgs in
-#eval (⊞ (i j k : Fin 2) => (IndexType.toFin (i,j,k)).toFloat).mapMono (fun x => sqrt x)
+#eval (⊞ (i j k : Fin 2) => (IndexType.toFin (i,j,k)).1.toFloat).mapMono (fun x => sqrt x)
 
 /-- info: ⊞[0.000000, 1.000000, 1.414214] -/
 #guard_msgs in
-#eval (0 : Float^[3]) |>.mapIdxMono (fun i _ => i.toFloat) |>.mapMono (fun x => sqrt x)
+#eval (0 : Float^[3]) |>.mapIdxMono (fun i _ => i.1.toFloat) |>.mapMono (fun x => sqrt x)
 
 
 /-- info: 6.000000 -/
 #guard_msgs in
-#eval ⊞[(1.0 : Float),2.0,3.0].fold (·+·) 0
+#eval ⊞[(1.0 : Float),2.0,3.0].foldl (·+·) 0
 
 /-- info: 1.000000 -/
 #guard_msgs in
 #eval ⊞[(1.0 :Float),2.0,3.0].reduce (min · ·)
 
 
-def softMax {I} [IndexType I]
+def softMax {I : Type} [IndexType I]
   (r : Float) (x : Float^[I]) : Float^[I] := Id.run do
   let m := x.reduce (max · ·)
   let x := x.mapMono fun x => x-m
@@ -86,7 +87,7 @@ def trace {n : Nat} (A : Float^[n,n]) :=
 --   ⊞ (i : Fin n) => ∑ j, w[j] * x[i-j]
 
 def Fin.shift {n} (i : Fin n) (j : ℤ) : Fin n :=
-    { val := ((i.1 + j) % n ).toNat, isLt := by sorry_proof }
+    { val := ((Int.ofNat i.1 + j) % n ).toNat, isLt := by sorry_proof }
 
 def conv1d {n : Nat} (k : Nat) (w : Float^[[-k:k]]) (x : Float^[n]) :=
     ⊞ (i : Fin n) => ∑ j, w[j] * x[i.shift j.1]
@@ -163,7 +164,7 @@ info: avgPool_v4 ⊞[1.0, 2.0, 3.0, 4.0, 5.0] ⋯ : Float^[2]
 #eval avgPool_v4 ⊞[1.0, 2.0, 3.0, 4.0]
 
 
-variable {I} [IndexType I] [DecidableEq I]
+variable {I : Type} [IndexType I] [DecidableEq I]
 
 def avgPool2d
     (x : Float^[I,n₁,n₂]) {m₁ m₂}
@@ -184,10 +185,10 @@ def avgPool2d
 def dense (n : Nat) (A : Float^[n,I]) (b : Float^[n]) (x : Float^[I]) : Float^[n] :=
   ⊞ (i : Fin n) => b[i] + ∑ j, A[i,j] * x[j]
 
-def SciLean.DataArrayN.resize3 (x : Float^[I]) (a b c : Nat) (h : a*b*c = IndexType.card I) :
+def SciLean.DataArrayN.resize3 (x : Float^[I]) (a b c : Nat) (h : a*b*c = size I) :
     Float^[a,b,c] :=
   { data := x.data ,
-    h_size := by simp[IndexType.card]; rw[← mul_assoc,←x.2,h] }
+    h_size := by simp[Size.size]; rw[← mul_assoc,←x.2,h] }
 
 def nnet := fun (w₁,b₁,w₂,b₂,w₃,b₃) (x : Float^[28,28]) =>
   x |>.resize3 1 28 28 (by decide)
@@ -198,3 +199,56 @@ def nnet := fun (w₁,b₁,w₂,b₂,w₃,b₃) (x : Float^[28,28]) =>
     |>.mapMono (fun x => max x 0)
     |> dense 10 w₃ b₃
     |> softMax 0.1
+
+
+----------------------------------------------------------------------------------------------------
+
+open Set
+
+local instance : VAdd Unit I :=
+  ⟨fun _ i => i⟩
+local instance [VAdd I K] [VAdd J L] : VAdd (I×J) (K×L) :=
+  ⟨fun (i,j) (k,l) => (i+ᵥk, j+ᵥl)⟩
+local instance [VAdd I K] [VAdd J L] : VAdd (I⊕J) (K×L) :=
+  ⟨fun ij (k,l) => match ij with | .inl i => (i+ᵥk, l) | .inr j => (k, j+ᵥl)⟩
+
+
+local instance : VAdd ℤ (Fin n) := ⟨fun i j => ⟨((Int.ofNat j.1 + i)%n).toNat, sorry_proof⟩⟩
+local instance (a b : ℤ) : VAdd (Set.Icc a b) (Fin n) := ⟨fun i j => i.1+ᵥj⟩
+local instance : VAdd (Fin k) (Fin n) := ⟨fun i j => ⟨((j.1 + i.1)%n), sorry_proof⟩⟩
+
+
+inductive hoho | neg | pos
+
+#check proxy_equiv% hoho
+
+
+def IndexType.ofEquiv [IndexType I] [Fintype J] [Size J] (eq : I ≃ J) : IndexType J where
+  next? := sorry
+  toFin := sorry
+  fromFin := sorry
+
+local instance : VAdd Bool (Fin n) :=
+  ⟨fun b i => match b with | false => (-1:ℤ)+ᵥi | true => (1:ℤ)+ᵥi⟩
+
+
+def outerproduct {I J : Type} [IndexType I] [IndexType J] (x : Float^[I]) (y : Float^[J]) :
+    Float^[I,J] :=
+  ⊞ i j => x[i] * y[j]
+
+
+-- ⊞[-1.0,1.0]
+def diff := (⊞ (b : Bool) => match b with | false => -1.0 | true => 1.0)
+def average := ⊞[0.25,0.5,0.25]
+
+#eval outerproduct diff average
+#eval outerproduct average diff
+
+#eval  outerproduct ⊞[-1.0,0,1.0] ⊞[0.25,0.5,0.25]
+#check outerproduct (outerproduct ⊞[0.25,0.5,0.25] ⊞[-1.0,0,1.0]) ⊞[0.25,0.5,0.25]
+
+-- X^[I] × X^[J] ≃ X^[I⊕J]
+-- outerproduct
+-- direcadd
+
+#synth VAdd (Bool × Fin 3) (Fin 10 × Fin 10)
diff --git a/todo.org b/todo.org
index 074fe4c1..ee0cbcef 100644
--- a/todo.org
+++ b/todo.org
@@ -68,7 +68,7 @@
 
 * Differentiability at point
 
-  Try define smoothenss/differentiability at a point. I really want to work with =1/x= without problems and assume that it is differentiable for every =x≠0=.
+  Try define smoothness/differentiability at a point. I really want to work with =1/x= without problems and assume that it is differentiable for every =x≠0=.
   
 * Machine learning
 
@@ -106,13 +106,13 @@
 
   - working with polynomials, differential forms, tensor products
 
-**  Goal is to get isomophisms:
+**  Goal is to get isomorphisms:
     
     𝓟[U×V, K] ≅ 𝓟[U, 𝓟[V, K]]
     
   - Using these isomorphisms we can get polynomial to a form 𝓟[ℝ, K] and on that we can define HornerForm is K has HornerForm
 
-  - In some sense these ismorphisms must be true:
+  - In some sense these isomorphisms must be true:
 
     𝓐[U×V, K] ≅ 𝓐[U, 𝓐[V, K]]
     
@@ -133,7 +133,7 @@
 * Approximating Spaces
 
   - Define abstract interface for a type to approximate another type
-  - will be usefull for creating finite elements, hybrid methods
+  - will be useful for creating finite elements, hybrid methods
     or finite elements
 
 * Manifolds through Quot