diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Append.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Append.lean
new file mode 100644
index 0000000..b3ebfef
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Append.lean
@@ -0,0 +1,595 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.DualIndex
+import HepLean.SpaceTime.LorentzTensor.Basic
+/-!
+
+# Appending index lists and consquences thereof.
+
+-/
+
+namespace IndexNotation
+
+
+namespace IndexList
+
+variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
+variable (l l2 : IndexList X)
+
+/-!
+
+## Appending index lists.
+
+-/
+
+instance : HAppend (IndexList X) (IndexList X) (IndexList X) :=
+    @instHAppendOfAppend (List (Index X)) List.instAppend
+
+def appendEquiv {l l2 : IndexList X} : Fin l.length ⊕ Fin l2.length ≃ Fin (l ++ l2).length :=
+  finSumFinEquiv.trans (Fin.castOrderIso (List.length_append _ _).symm).toEquiv
+
+@[simp]
+lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
+    (l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by
+  simp [appendEquiv, idMap]
+  rw [List.getElem_append_left]
+
+@[simp]
+lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
+    (l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by
+  simp [appendEquiv, idMap]
+  rw [List.getElem_append_right]
+  simp
+  omega
+  omega
+
+@[simp]
+lemma colorMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
+    (l ++ l2).colorMap (appendEquiv (Sum.inl i)) = l.colorMap i := by
+  simp [appendEquiv, colorMap]
+  rw [List.getElem_append_left]
+
+@[simp]
+lemma colorMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
+    (l ++ l2).colorMap (appendEquiv (Sum.inr i)) = l2.colorMap i := by
+  simp [appendEquiv, colorMap]
+  rw [List.getElem_append_right]
+  simp
+  omega
+  omega
+
+
+/-!
+
+## AreDualInSelf
+
+-/
+
+namespace AreDualInSelf
+
+@[simp]
+lemma append_inl_inl : (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inl j))
+    ↔ l.AreDualInSelf i j := by
+  simp [AreDualInSelf]
+
+@[simp]
+lemma append_inr_inr (l l2 : IndexList X) (i j : Fin l2.length) :
+    (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inr j))
+    ↔ l2.AreDualInSelf i j := by
+  simp [AreDualInSelf]
+
+@[simp]
+lemma append_inl_inr (l l2 : IndexList X) (i : Fin l.length) (j : Fin l2.length) :
+    (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inr j)) =
+    l.AreDualInOther l2 i j := by
+  simp [AreDualInSelf, AreDualInOther]
+
+@[simp]
+lemma append_inr_inl (l l2 : IndexList X) (i : Fin l2.length) (j : Fin l.length) :
+    (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inl j)) =
+    l2.AreDualInOther l i j := by
+  simp [AreDualInSelf, AreDualInOther]
+
+end AreDualInSelf
+
+
+/-!
+
+## Member withDual append conditions
+
+-/
+
+@[simp]
+lemma inl_mem_withDual_append_iff (i : Fin l.length) :
+    appendEquiv (Sum.inl i) ∈ (l ++ l2).withDual ↔ (i ∈ l.withDual ∨ i ∈ l.withDualInOther l2) := by
+  simp only [mem_withDual_iff_exists, mem_withInDualOther_iff_exists]
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · obtain ⟨j, hj⟩ := h
+    obtain ⟨k, hk⟩ := appendEquiv.surjective j
+    subst hk
+    match k with
+    | Sum.inl k =>
+      exact Or.inl ⟨k, by simpa using hj⟩
+    | Sum.inr k =>
+      exact Or.inr ⟨k, by simpa using hj⟩
+  · cases' h with h h <;>
+      obtain ⟨j, hj⟩ := h
+    · use appendEquiv (Sum.inl j)
+      simpa using hj
+    · use appendEquiv (Sum.inr j)
+      simpa using hj
+
+@[simp]
+lemma inr_mem_withDual_append_iff (i : Fin l2.length) :
+    appendEquiv (Sum.inr i) ∈ (l ++ l2).withDual
+    ↔ (i ∈ l2.withDual ∨ i ∈ l2.withDualInOther l) := by
+  simp only [mem_withDual_iff_exists, mem_withInDualOther_iff_exists]
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · obtain ⟨j, hj⟩ := h
+    obtain ⟨k, hk⟩ := appendEquiv.surjective j
+    subst hk
+    match k with
+    | Sum.inl k =>
+      exact Or.inr ⟨k, by simpa using hj⟩
+    | Sum.inr k =>
+      exact Or.inl ⟨k, by simpa using hj⟩
+  · cases' h with h h <;>
+      obtain ⟨j, hj⟩ := h
+    · use appendEquiv (Sum.inr j)
+      simpa using hj
+    · use appendEquiv (Sum.inl j)
+      simpa using hj
+
+def appendInlWithDual (i : l.withDual) : (l ++ l2).withDual :=
+  ⟨appendEquiv (Sum.inl i), by simp⟩
+
+
+/-!
+
+## getDual on appended lists
+
+-/
+
+@[simp]
+lemma getDual?_append_inl_withDual (i : l.withDual) :
+    (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inl (l.getDual! i))) := by
+  rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inl]
+  apply And.intro (l.areDualInSelf_getDual! i)
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  match k with
+  | Sum.inl k =>
+    simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
+      Fin.castOrderIso_apply, ge_iff_le]
+    rw [Fin.le_def]
+    have h2 := l.getDual?_eq_some_getDual! i
+    rw [getDual?, Fin.find_eq_some_iff] at h2
+    exact h2.2 k (by simpa using hj)
+  | Sum.inr k =>
+    simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
+      Fin.castOrderIso_apply, finSumFinEquiv_apply_right, ge_iff_le]
+    rw [Fin.le_def]
+    simp only [Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd]
+    omega
+
+@[simp]
+lemma getDual_append_inl_withDual (i : l.withDual) :
+    (l ++ l2).getDual ⟨appendEquiv (Sum.inl i), by simp⟩ =
+    ⟨appendEquiv (Sum.inl (l.getDual i)), by simp⟩ := by
+  simp [getDual, getDual!]
+
+@[simp]
+lemma getDual?_append_inl_not_withDual (i : Fin l.length) (hi : i ∉ l.withDual)
+    (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withDual) :
+    (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some
+      (appendEquiv (Sum.inr (l.getDualInOther! l2 ⟨i, by simp_all⟩)))  := by
+  rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inr]
+  apply And.intro (l.areDualInOther_getDualInOther! l2 ⟨i, by simp_all⟩)
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  match k with
+  | Sum.inl k =>
+    rw [AreDualInSelf.append_inl_inl] at hj
+    simp only [withDual, getDual?, Finset.mem_filter, Finset.mem_univ, true_and, Bool.not_eq_true,
+      Option.not_isSome, Option.isNone_iff_eq_none, Fin.find_eq_none_iff] at hi
+    exact False.elim (hi k hj)
+  | Sum.inr k =>
+    simp [appendEquiv]
+    rw [Fin.le_def]
+    have h1 := l.getDualInOther?_eq_some_getDualInOther! l2 ⟨i, by simp_all⟩
+    rw [getDualInOther?, Fin.find_eq_some_iff] at h1
+    simp only [Fin.coe_cast, Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le, ge_iff_le]
+    refine h1.2 k (by simpa using hj)
+
+@[simp]
+lemma getDual_append_inl_not_withDual (i : Fin l.length) (hi : i ∉ l.withDual)
+    (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withDual) :
+    (l ++ l2).getDual ⟨appendEquiv (Sum.inl i), h⟩ =
+    ⟨appendEquiv (Sum.inr (l.getDualInOther l2 ⟨i, by simp_all⟩)), by simp⟩ := by
+  simp [getDual, getDual!, getDual?_append_inl_not_withDual l l2 i hi h]
+  rfl
+
+@[simp]
+lemma getDual?_append_inr_withDualInOther (i : l2.withDualInOther l) :
+    (l ++ l2).getDual? (appendEquiv (Sum.inr i)) =
+    some (appendEquiv (Sum.inl (l2.getDualInOther! l i))) := by
+  rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inr_inl]
+  apply And.intro (l2.areDualInOther_getDualInOther! l ⟨i, by simp_all⟩)
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  match k with
+  | Sum.inl k =>
+    simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
+      Fin.castOrderIso_apply, ge_iff_le]
+    rw [Fin.le_def]
+    have h1 := l2.getDualInOther?_eq_some_getDualInOther! l ⟨i, by simp_all⟩
+    rw [getDualInOther?, Fin.find_eq_some_iff] at h1
+    simp only [Fin.coe_cast, Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le, ge_iff_le]
+    refine h1.2 k (by simpa using hj)
+  | Sum.inr k =>
+    simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
+      Fin.castOrderIso_apply, finSumFinEquiv_apply_right, ge_iff_le]
+    rw [Fin.le_def]
+    simp only [Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd]
+    omega
+
+@[simp]
+lemma getDual_append_inr_withDualInOther (i : l2.withDualInOther l) :
+    (l ++ l2).getDual ⟨appendEquiv (Sum.inr i), by simp⟩ =
+    ⟨appendEquiv (Sum.inl (l2.getDualInOther l i)), by simp⟩ := by
+  simp [getDual, getDual!]
+  rfl
+
+@[simp]
+lemma getDual?_append_inr_not_withDualInOther (i : Fin l2.length) (hi : i ∉ l2.withDualInOther l)
+    (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withDual) :
+    (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = some
+    (appendEquiv (Sum.inr (l2.getDual! ⟨i, by simp_all⟩))) := by
+  rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inr_inr]
+  apply And.intro (l2.areDualInSelf_getDual! ⟨i, by simp_all⟩)
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  match k with
+  | Sum.inl k =>
+    simp at hj
+    refine False.elim (hi ?_)
+    simp [withDualInOther, getDualInOther?, Fin.isSome_find_iff]
+    exact ⟨k, hj⟩
+  | Sum.inr k =>
+    simp [appendEquiv]
+    rw [Fin.le_def]
+    simp
+    have h2 := l2.getDual?_eq_some_getDual! ⟨i, by simp_all⟩
+    rw [getDual?, Fin.find_eq_some_iff] at h2
+    simp only [AreDualInSelf.append_inr_inr] at hj
+    exact h2.2 k hj
+
+@[simp]
+lemma getDual_append_inr_not_withDualInOther (i : Fin l2.length) (hi : i ∉ l2.withDualInOther l)
+    (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withDual) :
+    (l ++ l2).getDual ⟨appendEquiv (Sum.inr i), h⟩ =
+    ⟨appendEquiv (Sum.inr (l2.getDual ⟨i, by simp_all⟩)), by simp⟩ := by
+  simp [getDual, getDual!, getDual?_append_inr_not_withDualInOther l l2 i hi h]
+
+
+@[simp]
+lemma getDual?_append_inl (i : Fin l.length) : (l ++ l2).getDual? (appendEquiv (Sum.inl i)) =
+    Option.or (Option.map (appendEquiv ∘ Sum.inl) (l.getDual? i))
+    (Option.map (appendEquiv ∘ Sum.inr) (l.getDualInOther? l2 i)) := by
+  by_cases h : (appendEquiv (Sum.inl i)) ∈ (l ++ l2).withDual
+  · by_cases hl : i ∈ l.withDual
+    · rw [(l ++ l2).getDual?_eq_some_getDual! ⟨(appendEquiv (Sum.inl i)), h⟩]
+      rw [l.getDual?_eq_some_getDual! ⟨i, hl⟩]
+      rw [getDual!]
+      simp only [Option.some_get, Option.map_some', Function.comp_apply, Option.or_some]
+      exact getDual?_append_inl_withDual l l2 ⟨i, hl⟩
+    · let h' := h
+      rw [l.getDual?_eq_none_on_not_mem i hl]
+      simp only [inl_mem_withDual_append_iff] at h
+      simp_all only [false_or, Option.map_none', Option.none_or]
+      rw [l.getDualInOther?_eq_some_getDualInOther! l2 ⟨i, h⟩]
+      rw [getDual?_append_inl_not_withDual l l2 i hl h']
+      rfl
+  · rw [(l ++ l2).getDual?_eq_none_on_not_mem _ h]
+    simp only [inl_mem_withDual_append_iff, not_or, not_exists] at h
+    rw [l.getDual?_eq_none_on_not_mem _ h.1, l.getDualInOther?_eq_none_on_not_mem l2 _ h.2]
+    rfl
+
+@[simp]
+lemma getDual?_append_inr (i : Fin l2.length) :
+    (l ++ l2).getDual? (appendEquiv (Sum.inr i)) =
+    Option.or (Option.map (appendEquiv ∘ Sum.inl) (l2.getDualInOther? l i))
+    (Option.map (appendEquiv ∘ Sum.inr) (l2.getDual? i)) := by
+  by_cases h : (appendEquiv (Sum.inr i)) ∈ (l ++ l2).withDual
+  · by_cases hl1 : i ∈ l2.withDualInOther l
+    · rw [(l ++ l2).getDual?_eq_some_getDual! ⟨(appendEquiv (Sum.inr i)), h⟩]
+      rw [l2.getDualInOther?_eq_some_getDualInOther! l ⟨i, hl1⟩]
+      rw [getDual!]
+      simp only [Option.some_get, Option.map_some', Function.comp_apply, Option.or_some]
+      exact getDual?_append_inr_withDualInOther l l2 ⟨i, hl1⟩
+    · have h' := h
+      rw [l2.getDualInOther?_eq_none_on_not_mem l i hl1]
+      simp only [inr_mem_withDual_append_iff, not_exists] at h hl1
+      simp_all only [not_exists, exists_false, or_false,
+        Option.map_none', Option.none_or]
+      rw [l2.getDual?_eq_some_getDual! ⟨i, h⟩]
+      simp only [Option.map_some', Function.comp_apply]
+      exact getDual?_append_inr_not_withDualInOther l l2 i hl1 h'
+  · rw [(l ++ l2).getDual?_eq_none_on_not_mem _ h]
+    simp only [inr_mem_withDual_append_iff, not_or, not_exists] at h
+    rw [l2.getDual?_eq_none_on_not_mem _ h.1, l2.getDualInOther?_eq_none_on_not_mem l _ h.2]
+    rfl
+
+
+/-!
+
+## withUniqueDualInOther append conditions
+
+-/
+
+lemma append_inl_not_mem_withDual_of_withDualInOther (i : Fin l.length)
+    (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) :
+    i ∈ l.withDual ↔ ¬ i ∈ l.withDualInOther l2 := by
+  apply Iff.intro
+  · intro hs
+    by_contra ho
+    obtain ⟨j, hj⟩ := (l.mem_withDual_iff_exists).mp hs
+    obtain ⟨k, hk⟩ := (l.mem_withInDualOther_iff_exists l2).mp ho
+    have h1 : appendEquiv (Sum.inl j) = appendEquiv (Sum.inr k) := by
+      refine (l ++ l2).eq_of_areDualInSelf_withUniqueDual ⟨appendEquiv (Sum.inl i), h⟩ ?_ ?_
+      simpa using hj
+      simpa using hk
+    simp at h1
+  · intro ho
+    by_contra hs
+    have h1 :  appendEquiv (Sum.inl i) ∈ (l ++ l2).withDual := by
+      exact (l ++ l2).mem_withDual_of_withUniqueDual ⟨appendEquiv (Sum.inl i), h⟩
+    obtain ⟨j, hj⟩ := ((l ++ l2).mem_withDual_iff_exists).mp h1
+    obtain ⟨k, hk⟩ := appendEquiv.surjective j
+    subst hk
+    match k with
+    | Sum.inl k =>
+      rw [mem_withDual_iff_exists] at hs
+      simp_all
+    | Sum.inr k =>
+      rw [mem_withInDualOther_iff_exists] at ho
+      simp_all
+
+lemma append_inr_not_mem_withDual_of_withDualInOther (i : Fin l2.length)
+    (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) :
+    i ∈ l2.withDual ↔ ¬ i ∈ l2.withDualInOther l := by
+  apply Iff.intro
+  · intro hs
+    by_contra ho
+    obtain ⟨j, hj⟩ := (l2.mem_withDual_iff_exists).mp hs
+    obtain ⟨k, hk⟩ := (l2.mem_withInDualOther_iff_exists l).mp ho
+    have h1 : appendEquiv (Sum.inr j) = appendEquiv (Sum.inl k) := by
+      refine (l ++ l2).eq_of_areDualInSelf_withUniqueDual ⟨appendEquiv (Sum.inr i), h⟩ ?_ ?_
+      simpa using hj
+      simpa using hk
+    simp at h1
+  · intro ho
+    by_contra hs
+    have h1 :  appendEquiv (Sum.inr i) ∈ (l ++ l2).withDual := by
+      exact (l ++ l2).mem_withDual_of_withUniqueDual ⟨appendEquiv (Sum.inr i), h⟩
+    obtain ⟨j, hj⟩ := ((l ++ l2).mem_withDual_iff_exists).mp h1
+    obtain ⟨k, hk⟩ := appendEquiv.surjective j
+    subst hk
+    match k with
+    | Sum.inl k =>
+      rw [mem_withInDualOther_iff_exists] at ho
+      simp_all
+    | Sum.inr k =>
+      rw [mem_withDual_iff_exists] at hs
+      simp_all
+
+
+lemma append_inr_mem_withUniqueDual_of_append_inl (i : Fin l.length)
+    (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) :
+    appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDual := by
+  have hinj : Function.Injective (Option.map (@appendEquiv _ _ l l2 ∘ Sum.inr)) := by
+          apply Option.map_injective
+          rw [@Equiv.comp_injective]
+          exact Sum.inr_injective
+  let h' := h
+  simp [withUniqueDual] at h ⊢
+  apply And.intro h.1
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  match k with
+  | Sum.inl k =>
+    have h1 := h.2 (appendEquiv (Sum.inr k))
+    simp at h1 hj
+    have h2 := h1 hj
+    by_cases hs : i ∈ l.withDual <;> rename_i hs
+    · rw [l.getDual?_eq_some_getDual! ⟨i, hs⟩] at h2
+      simp at h2
+    · rw [l.getDual?_eq_none_on_not_mem i hs] at h2
+      simp at h2
+      rw [← Option.map_some', ← Option.map_some', Option.map_map] at h2
+      rw [← hinj h2]
+      rfl
+  | Sum.inr k =>
+    have h1 := h.2 (appendEquiv (Sum.inl k))
+    simp at h1 hj
+    have h2 := h1 hj
+    by_cases hs : i ∈ l.withDual <;> rename_i hs
+    · rw [l.getDual?_eq_some_getDual! ⟨i, hs⟩] at h2
+      simp only [Option.map_some', Function.comp_apply, Option.or_some, Option.some.injEq,
+        EmbeddingLike.apply_eq_iff_eq, Sum.inl.injEq] at h2
+      have ho := (l.append_inl_not_mem_withDual_of_withDualInOther l2 i h').mp hs
+      rw [l.getDualInOther?_eq_none_on_not_mem _ _ ho]
+      simp only [Option.map_none', Option.none_or]
+      rw [← Option.map_some', ← Option.map_some', Option.map_map, h2]
+      simp [some_dual!_eq_gual?]
+    · have ho := (l.append_inl_not_mem_withDual_of_withDualInOther l2 i h').mpr.mt hs
+      simp at ho
+      rw [l.getDualInOther?_eq_some_getDualInOther! l2 ⟨i, ho⟩] at h2 ⊢
+      simp at h2
+      simp
+      rw [l.getDual?_eq_none_on_not_mem _ hs] at h2
+      simp at h2
+
+lemma withUniqueDual_iff_not_withUniqueDualInOther_of_inl_withUniqueDualInOther
+    (i : Fin l.length) (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) :
+    i ∈ l.withUniqueDual ↔ ¬ i ∈ l.withUniqueDualInOther l2 := by
+  have h' := h
+  rw [withUniqueDual] at h
+  simp only [Finset.mem_filter, Finset.mem_univ, inl_mem_withDual_append_iff,
+    getDual?_append_inl, true_and] at h
+  simp [withUniqueDual, withUniqueDualInOther]
+  cases' h.1 with h1 h1
+  · simp [h1]
+    intro j hj
+    have hj' := h.2 (appendEquiv (Sum.inl j))
+    simp at hj'
+    have hj'' := hj' hj
+    rw [l.getDual?_eq_some_getDual! ⟨i, by rw [mem_withDual_iff_exists]; exact ⟨j, hj⟩⟩] at hj'' ⊢
+    simpa using hj''
+  · have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h'
+    simp_all
+    intro j hj
+    have hj' := h (appendEquiv (Sum.inr j))
+    simp at hj'
+    have hj'' := hj' hj
+    rw [l.getDual?_eq_none_on_not_mem _ hn] at hj''
+    simp at hj''
+    rw [l.getDualInOther?_eq_some_getDualInOther!
+      l2 ⟨i, by rw [mem_withInDualOther_iff_exists]; exact ⟨j, hj⟩⟩] at hj'' ⊢
+    simpa using hj''
+
+lemma withUniqueDual_iff_not_withUniqueDualInOther_of_inr_withUniqueDualInOther
+    (i : Fin l2.length) (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) :
+    i ∈ l2.withUniqueDual ↔ ¬ i ∈ l2.withUniqueDualInOther l := by
+  have h' := h
+  rw [withUniqueDual] at h
+  simp only [Finset.mem_filter, Finset.mem_univ, inr_mem_withDual_append_iff, getDual?_append_inr,
+    true_and] at h
+  simp [withUniqueDual, withUniqueDualInOther]
+  cases' h.1 with h1 h1
+  · have hn := (l.append_inr_not_mem_withDual_of_withDualInOther l2 i h').mp h1
+    simp [h1]
+    intro j hj
+    have hj' := h.2 (appendEquiv (Sum.inr j))
+    simp at hj'
+    have hj'' := hj' hj
+    rw [l2.getDual?_eq_some_getDual! ⟨i, by rw [mem_withDual_iff_exists]; exact ⟨j, hj⟩⟩] at hj'' ⊢
+    rw [l2.getDualInOther?_eq_none_on_not_mem _ _ hn] at hj''
+    simpa using hj''
+  · have hn := l.append_inr_not_mem_withDual_of_withDualInOther l2 i h'
+    simp_all
+    intro j hj
+    have hj' := h (appendEquiv (Sum.inl j))
+    simp at hj'
+    have hj'' := hj' hj
+    rw [l2.getDual?_eq_none_on_not_mem _ hn] at hj''
+    simp at hj''
+    rw [l2.getDualInOther?_eq_some_getDualInOther!
+      l ⟨i, by rw [mem_withInDualOther_iff_exists]; exact ⟨j, hj⟩⟩] at hj'' ⊢
+    simpa using hj''
+
+lemma append_inl_mem_withUniqueDual_of_withUniqueDual (i : Fin l.length)
+    (h : i ∈ l.withUniqueDual) (hn : i ∉ l.withDualInOther l2) :
+    appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by
+  simp [withUniqueDual]
+  apply And.intro (Or.inl (l.mem_withDual_of_withUniqueDual ⟨i, h⟩))
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  match k with
+  | Sum.inl k =>
+    rw [l.getDual?_eq_some_getDual! ⟨i, l.mem_withDual_of_withUniqueDual ⟨i, h⟩⟩]
+    simp
+    rw [← l.eq_getDual_of_withUniqueDual_iff ⟨i, h⟩ k]
+    simpa using hj
+  | Sum.inr k =>
+    simp at hj
+    refine False.elim (hn ?_)
+    exact (l.mem_withInDualOther_iff_exists _).mpr ⟨k, hj⟩
+
+lemma append_inl_mem_of_withUniqueDualInOther (i : Fin l.length) (ho : i ∈ l.withUniqueDualInOther l2) :
+    appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by
+  simp [withUniqueDual]
+  apply And.intro (Or.inr (l.mem_withDualInOther_of_withUniqueDualInOther l2 ⟨i, ho⟩))
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  have hs := l.not_mem_withDual_of_withUniqueDualInOther l2 ⟨i, ho⟩
+  rw [l.getDual?_eq_none_on_not_mem _ hs]
+  rw [l.getDualInOther?_eq_some_getDualInOther! l2
+      ⟨i, (l.mem_withDualInOther_of_withUniqueDualInOther l2 ⟨i, ho⟩)⟩]
+  match k with
+  | Sum.inl k =>
+    refine False.elim (hs ?_)
+    simp at hj
+    exact (l.mem_withDual_iff_exists).mpr ⟨k, hj⟩
+  | Sum.inr k =>
+    simp at hj
+    simp
+    erw [← l.eq_getDualInOther_of_withUniqueDual_iff l2 ⟨i, ho⟩ k]
+    simpa using hj
+
+@[simp]
+lemma append_inl_mem_withUniqueDual_iff (i : Fin l.length) :
+    appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual ↔
+    ((i ∈ l.withUniqueDual ∧ i ∉ l.withDualInOther l2) ↔ ¬ i ∈ l.withUniqueDualInOther l2) := by
+  apply Iff.intro
+  · intro h
+    apply Iff.intro
+    · intro hs
+      exact (l.withUniqueDual_iff_not_withUniqueDualInOther_of_inl_withUniqueDualInOther l2 i
+        h).mp hs.1
+    · intro ho
+      have hs := ((l.withUniqueDual_iff_not_withUniqueDualInOther_of_inl_withUniqueDualInOther l2 i
+        h).mpr ho)
+      apply And.intro hs
+      refine (l.append_inl_not_mem_withDual_of_withDualInOther l2 i h).mp ?_
+      exact (l.mem_withDual_of_withUniqueDual ⟨i, hs⟩)
+  · intro h
+    by_cases ho : i ∈ l.withUniqueDualInOther l2
+    · exact append_inl_mem_of_withUniqueDualInOther l l2 i ho
+    · exact append_inl_mem_withUniqueDual_of_withUniqueDual l l2 i (h.mpr ho).1 (h.mpr ho).2
+
+lemma append_inl_mem_withUniqueDual_of_append_inr (i : Fin l.length)
+    (h : appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDual) :
+    appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by
+  simp
+  apply Iff.intro
+  · intro hs
+    exact (l2.withUniqueDual_iff_not_withUniqueDualInOther_of_inr_withUniqueDualInOther
+      l i h).mp hs.1
+  · intro ho
+    have hs := (l2.withUniqueDual_iff_not_withUniqueDualInOther_of_inr_withUniqueDualInOther
+      l i h).mpr ho
+    apply And.intro hs
+    refine (l2.append_inr_not_mem_withDual_of_withDualInOther l i h).mp ?_
+    exact (l.mem_withDual_of_withUniqueDual ⟨i, hs⟩)
+
+  lemma append_mem_withUniqueDual_symm (i : Fin l.length) :
+      appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual ↔
+      appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDual := by
+    apply Iff.intro
+    · intro h'
+      exact append_inr_mem_withUniqueDual_of_append_inl l l2 i h'
+    · intro h'
+      exact append_inl_mem_withUniqueDual_of_append_inr l l2 i h'
+
+@[simp]
+lemma append_inr_mem_withUniqueDual_iff (i : Fin l2.length) :
+    appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual ↔
+    ((i ∈ l2.withUniqueDual ∧ i ∉ l2.withDualInOther l) ↔ ¬ i ∈ l2.withUniqueDualInOther l) := by
+  rw [← append_mem_withUniqueDual_symm]
+  simp
+
+
+end IndexList
+
+end IndexNotation
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
index 7641b43..9529798 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
@@ -191,10 +191,10 @@ def colorMap : Fin l.numIndices → X :=
   fun i => (l.get i).toColor
 
 /-- The map of from `Fin s.numIndices` into the natural numbers associated to an index list. -/
-def idMap : Fin l.numIndices → Nat :=
+def idMap : Fin l.length → Nat :=
   fun i => (l.get i).id
 
-lemma idMap_cast {l1 l2 : IndexList X} (h : l1 = l2) (i : Fin l1.numIndices) :
+lemma idMap_cast {l1 l2 : IndexList X} (h : l1 = l2) (i : Fin l1.length) :
     l1.idMap i = l2.idMap (Fin.cast (by rw [h]) i) := by
   subst h
   rfl
@@ -249,47 +249,6 @@ lemma fromFinMap_numIndices {n : ℕ} (f : Fin n → Index X) :
   simp [fromFinMap, numIndices]
 
 
-/-!
-
-## Appending index lists.
-
--/
-instance : HAppend (IndexList X) (IndexList X) (IndexList X) :=
-    @instHAppendOfAppend (List (Index X)) List.instAppend
-
-def appendEquiv {l l2 : IndexList X} : Fin l.length ⊕ Fin l2.length ≃ Fin (l ++ l2).length :=
-  finSumFinEquiv.trans (Fin.castOrderIso (List.length_append _ _).symm).toEquiv
-
-@[simp]
-lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
-    (l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by
-  simp [appendEquiv, idMap]
-  rw [List.getElem_append_left]
-
-@[simp]
-lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
-    (l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by
-  simp [appendEquiv, idMap]
-  rw [List.getElem_append_right]
-  simp
-  omega
-  omega
-
-@[simp]
-lemma colorMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
-    (l ++ l2).colorMap (appendEquiv (Sum.inl i)) = l.colorMap i := by
-  simp [appendEquiv, colorMap]
-  rw [List.getElem_append_left]
-
-@[simp]
-lemma colorMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
-    (l ++ l2).colorMap (appendEquiv (Sum.inr i)) = l2.colorMap i := by
-  simp [appendEquiv, colorMap]
-  rw [List.getElem_append_right]
-  simp
-  omega
-  omega
-
 end IndexList
 
 end IndexNotation
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/DualIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/DualIndex.lean
index 2bc0efd..11879aa 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/DualIndex.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/DualIndex.lean
@@ -32,11 +32,11 @@ def AreDualInSelf (i j : Fin l.length) : Prop :=
 instance (i j : Fin l.length) : Decidable (l.AreDualInSelf i j) :=
   instDecidableAnd
 
-def AreDualInOther {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) :
+def AreDualInOther  (i : Fin l.length) (j : Fin l2.length) :
     Prop := l.idMap i = l2.idMap j
 
 instance {l : IndexList X} {l2 : IndexList X}  (i : Fin l.length) (j : Fin l2.length) :
-    Decidable (AreDualInOther i j) := (l.idMap i).decEq (l2.idMap j)
+    Decidable (l.AreDualInOther l2 i j) := (l.idMap i).decEq (l2.idMap j)
 
 
 namespace AreDualInSelf
@@ -52,29 +52,6 @@ lemma symm (h : l.AreDualInSelf i j) : l.AreDualInSelf j i := by
 lemma self_false (i : Fin l.length) : ¬ l.AreDualInSelf i i := by
   simp [AreDualInSelf]
 
-@[simp]
-lemma append_inl_inl : (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inl j))
-    ↔ l.AreDualInSelf i j := by
-  simp [AreDualInSelf]
-
-@[simp]
-lemma append_inr_inr (l l2 : IndexList X) (i j : Fin l2.length) :
-    (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inr j))
-    ↔ l2.AreDualInSelf i j := by
-  simp [AreDualInSelf]
-
-@[simp]
-lemma append_inl_inr (l l2 : IndexList X) (i : Fin l.length) (j : Fin l2.length) :
-    (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inr j)) =
-    AreDualInOther i j := by
-  simp [AreDualInSelf, AreDualInOther]
-
-@[simp]
-lemma append_inr_inl (l l2 : IndexList X) (i : Fin l2.length) (j : Fin l.length) :
-    (l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inl j)) =
-    AreDualInOther i j := by
-  simp [AreDualInSelf, AreDualInOther]
-
 end AreDualInSelf
 
 namespace AreDualInOther
@@ -82,7 +59,7 @@ namespace AreDualInOther
 variable {l l2 : IndexList X} {i : Fin l.length} {j : Fin l2.length}
 
 @[symm]
-lemma symm  (h : AreDualInOther i j) : AreDualInOther j i := by
+lemma symm  (h : l.AreDualInOther l2 i j) : l2.AreDualInOther l j i := by
   rw [AreDualInOther] at h ⊢
   exact h.symm
 
@@ -90,13 +67,552 @@ end AreDualInOther
 
 /-!
 
+## The getDual? Function
+
+-/
+
+/-- Given an `i`, if a dual exists in the same list,
+   outputs the first such dual, otherwise outputs `none`. -/
+def getDual? (i : Fin l.length) : Option (Fin l.length) :=
+  Fin.find (fun j => l.AreDualInSelf i j)
+
+/-- Given an `i`, if a dual exists in the other list,
+   outputs the first such dual, otherwise outputs `none`. -/
+def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) :=
+  Fin.find (fun j => l.AreDualInOther l2 i j)
+
+/-!
+
+## With dual self.
+
+-/
+
+def withDual : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDual? i).isSome) Finset.univ
+
+lemma mem_withDual_iff_exists : i ∈ l.withDual ↔ ∃ j, l.AreDualInSelf i j := by
+  simp [withDual, Finset.mem_filter, Finset.mem_univ, getDual?]
+  rw [Fin.isSome_find_iff]
+
+lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
+    l.getDual? j = i ∨ l.getDual? i = j ∨ l.getDual? j = l.getDual? i := by
+  have h3 : (l.getDual? i).isSome := by
+    simpa [getDual?, Fin.isSome_find_iff] using ⟨j, h⟩
+  obtain ⟨k, hk⟩ := Option.isSome_iff_exists.mp h3
+  rw [hk]
+  rw [getDual?, Fin.find_eq_some_iff] at hk
+  by_cases hik : i < k
+  · apply Or.inl
+    rw [getDual?, Fin.find_eq_some_iff]
+    apply And.intro h.symm
+    intro k' hk'
+    by_cases hik' : i = k'
+    subst hik'
+    rfl
+    have hik'' :  l.AreDualInSelf i k' := by
+      simp [AreDualInSelf, hik']
+      simp_all [AreDualInSelf]
+    have hk'' := hk.2 k' hik''
+    exact (lt_of_lt_of_le hik hk'').le
+  · by_cases hjk : j ≤ k
+    · apply Or.inr
+      apply Or.inl
+      have hj := hk.2 j h
+      simp
+      omega
+    · apply Or.inr
+      apply Or.inr
+      rw [getDual?, Fin.find_eq_some_iff]
+      apply And.intro
+      · simp_all [AreDualInSelf]
+        exact Fin.ne_of_gt hjk
+      intro k' hk'
+      by_cases hik' : i = k'
+      subst hik'
+      exact Lean.Omega.Fin.le_of_not_lt hik
+      have hik'' :  l.AreDualInSelf i k' := by
+        simp [AreDualInSelf, hik']
+        simp_all [AreDualInSelf]
+      exact hk.2 k' hik''
+
+
+def getDual! (i : l.withDual) : Fin l.length :=
+  (l.getDual? i).get (by simpa [withDual] using i.2)
+
+lemma getDual?_eq_some_getDual! (i : l.withDual) : l.getDual? i = some (l.getDual! i) := by
+  simp [getDual!]
+
+lemma getDual?_eq_none_on_not_mem (i : Fin l.length) (h : i ∉ l.withDual) :
+    l.getDual? i = none := by
+  simpa [withDual, getDual?, Fin.find_eq_none_iff]  using h
+
+lemma some_dual!_eq_gual? (i : l.withDual) : some (l.getDual! i) = l.getDual? i := by
+  rw [getDual?_eq_some_getDual!]
+
+lemma areDualInSelf_getDual! (i : l.withDual) : l.AreDualInSelf i (l.getDual! i) := by
+  have h := l.getDual?_eq_some_getDual! i
+  rw [getDual?, Fin.find_eq_some_iff] at h
+  exact h.1
+
+@[simp]
+lemma getDual!_id (i : l.withDual) : l.idMap (l.getDual! i) = l.idMap i := by
+  simpa using (l.areDualInSelf_getDual! i).2.symm
+
+lemma getDual_mem_withDual (i : l.withDual) : l.getDual! i ∈ l.withDual := by
+  simp only [withDual, Finset.mem_filter, Finset.mem_univ, true_and]
+  rw [getDual?, Fin.isSome_find_iff]
+  exact ⟨i, (l.areDualInSelf_getDual! i).symm⟩
+
+def getDual (i : l.withDual) : l.withDual := ⟨l.getDual! i, l.getDual_mem_withDual i⟩
+
+@[simp]
+lemma getDual_id (i : l.withDual) :
+    l.idMap (l.getDual i) = l.idMap i := by
+  simp [getDual]
+
+/-!
+
+## With dual other.
+
+-/
+
+def withDualInOther : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDualInOther? l2 i).isSome) Finset.univ
+
+lemma mem_withInDualOther_iff_exists :
+    i ∈ l.withDualInOther l2 ↔ ∃ (j : Fin l2.length), l.AreDualInOther l2 i j := by
+  simp [withDualInOther, Finset.mem_filter, Finset.mem_univ, getDualInOther?]
+  rw [Fin.isSome_find_iff]
+
+def getDualInOther! (i : l.withDualInOther l2) : Fin l2.length :=
+  (l.getDualInOther? l2 i).get (by simpa [withDualInOther] using i.2)
+
+
+lemma getDualInOther?_eq_some_getDualInOther! (i : l.withDualInOther l2) :
+    l.getDualInOther? l2 i = some (l.getDualInOther! l2 i) := by
+  simp [getDualInOther!]
+
+lemma getDualInOther?_eq_none_on_not_mem (i : Fin l.length) (h : i ∉ l.withDualInOther l2) :
+    l.getDualInOther? l2 i = none := by
+  simpa [getDualInOther?, Fin.find_eq_none_iff, mem_withInDualOther_iff_exists]  using h
+
+
+lemma areDualInOther_getDualInOther! (i : l.withDualInOther l2) :
+    l.AreDualInOther l2 i (l.getDualInOther! l2 i) := by
+  have h := l.getDualInOther?_eq_some_getDualInOther! l2 i
+  rw [getDualInOther?, Fin.find_eq_some_iff] at h
+  exact h.1
+
+@[simp]
+lemma getDualInOther!_id (i : l.withDualInOther l2) :
+    l2.idMap (l.getDualInOther! l2 i) = l.idMap i := by
+  simpa using (l.areDualInOther_getDualInOther! l2 i).symm
+
+lemma getDualInOther_mem_withDualInOther (i : l.withDualInOther l2) :
+    l.getDualInOther! l2 i ∈ l2.withDualInOther l :=
+  (l2.mem_withInDualOther_iff_exists l).mpr ⟨i, (areDualInOther_getDualInOther! l l2 i).symm⟩
+
+def getDualInOther (i : l.withDualInOther l2) : l2.withDualInOther l :=
+  ⟨l.getDualInOther! l2 i, l.getDualInOther_mem_withDualInOther l2 i⟩
+
+@[simp]
+lemma getDualInOther_id (i : l.withDualInOther l2) :
+    l2.idMap (l.getDualInOther l2 i) = l.idMap i := by
+  simp [getDualInOther]
+
+lemma getDualInOther_coe (i : l.withDualInOther l2) :
+    (l.getDualInOther l2 i).1 = l.getDualInOther! l2 i := by
+  rfl
+
+
+/-!
+
+## Has single dual in self.
+
+-/
+
+
+def withUniqueDual : Finset (Fin l.length) :=
+  Finset.filter (fun i => i ∈ l.withDual ∧
+    ∀ j, l.AreDualInSelf i j → j = l.getDual? i) Finset.univ
+
+lemma mem_withDual_of_withUniqueDual (i : l.withUniqueDual) :
+    i.1 ∈ l.withDual := by
+  have hi := i.2
+  simp [withUniqueDual, Finset.mem_filter, Finset.mem_univ] at hi
+  exact hi.1
+
+def fromWithUnique (i : l.withUniqueDual) : l.withDual :=
+  ⟨i.1, l.mem_withDual_of_withUniqueDual i⟩
+
+instance : Coe l.withUniqueDual l.withDual where
+  coe i := ⟨i.1, l.mem_withDual_of_withUniqueDual i⟩
+
+@[simp]
+lemma fromWithUnique_coe (i : l.withUniqueDual) : (l.fromWithUnique i).1 = i.1 := by
+  rfl
+
+lemma all_dual_eq_getDual_of_withUniqueDual (i : l.withUniqueDual) :
+    ∀ j, l.AreDualInSelf i j → j = l.getDual! i := by
+  have hi := i.2
+  simp [withUniqueDual] at hi
+  intro j hj
+  simpa [getDual!, fromWithUnique] using (Option.get_of_mem _ (hi.2 j hj ).symm).symm
+
+lemma eq_of_areDualInSelf_withUniqueDual {j k : Fin l.length} (i : l.withUniqueDual)
+    (hj : l.AreDualInSelf i j) (hk : l.AreDualInSelf i k) :
+    j = k := by
+  have hj' := all_dual_eq_getDual_of_withUniqueDual l i j hj
+  have hk' := all_dual_eq_getDual_of_withUniqueDual l i k hk
+  rw [hj', hk']
+
+lemma eq_getDual_of_withUniqueDual_iff (i : l.withUniqueDual) (j : Fin l.length) :
+    l.AreDualInSelf i j ↔ j = l.getDual! i := by
+  apply Iff.intro
+  intro h
+  exact (l.all_dual_eq_getDual_of_withUniqueDual i) j h
+  intro h
+  subst h
+  exact areDualInSelf_getDual! l i
+
+@[simp]
+lemma getDual!_getDual_of_withUniqueDual (i : l.withUniqueDual) :
+    l.getDual! (l.getDual i) = i := by
+  by_contra hn
+  have h' : l.AreDualInSelf i (l.getDual! (l.getDual i)) := by
+    simp [AreDualInSelf, hn]
+    simp_all [AreDualInSelf, getDual, fromWithUnique]
+    exact fun a => hn (id (Eq.symm a))
+  rw [eq_getDual_of_withUniqueDual_iff] at h'
+  have hx := l.areDualInSelf_getDual! (l.getDual i)
+  simp_all [getDual]
+
+@[simp]
+lemma getDual_getDual_of_withUniqueDual (i : l.withUniqueDual) :
+    l.getDual (l.getDual i) = l.fromWithUnique i :=
+  SetCoe.ext (getDual!_getDual_of_withUniqueDual l i)
+
+@[simp]
+lemma getDual?_getDual!_of_withUniqueDual (i : l.withUniqueDual) :
+    l.getDual? (l.getDual! i) = some i := by
+  change l.getDual? (l.getDual i) = some i
+  rw [getDual?_eq_some_getDual!]
+  simp
+
+@[simp]
+lemma getDual?_getDual?_of_withUniqueDualInOther (i : l.withUniqueDual) :
+    (l.getDual? i).bind l.getDual? = some i := by
+  rw [getDual?_eq_some_getDual! l i]
+  simp
+
+
+lemma getDual_of_withUniqueDual_mem (i : l.withUniqueDual) :
+    l.getDual! i ∈ l.withUniqueDual := by
+  simp [withUniqueDual]
+  apply And.intro (getDual_mem_withDual l ⟨↑i, mem_withDual_of_withUniqueDual l i⟩)
+  intro j hj
+  have h1 : i = j := by
+    by_contra hn
+    have h' : l.AreDualInSelf i j := by
+      simp [AreDualInSelf, hn]
+      simp_all [AreDualInSelf, getDual, fromWithUnique]
+    rw [eq_getDual_of_withUniqueDual_iff] at h'
+    subst h'
+    simp_all [getDual]
+  subst h1
+  rfl
+
+def getDualEquiv : l.withUniqueDual ≃ l.withUniqueDual where
+  toFun x := ⟨l.getDual x, l.getDual_of_withUniqueDual_mem x⟩
+  invFun x := ⟨l.getDual x, l.getDual_of_withUniqueDual_mem x⟩
+  left_inv x := SetCoe.ext (by
+    simp only [Subtype.coe_eta, getDual_getDual_of_withUniqueDual]
+    rfl)
+  right_inv x := SetCoe.ext (by
+    simp only [Subtype.coe_eta, getDual_getDual_of_withUniqueDual]
+    rfl)
+
+@[simp]
+lemma getDualEquiv_involutive : Function.Involutive l.getDualEquiv := by
+  intro x
+  simp [getDualEquiv, fromWithUnique]
+
+
+/-!
+
+## Has single in other.
+
+-/
+
+def withUniqueDualInOther : Finset (Fin l.length) :=
+  Finset.filter (fun i => i ∉ l.withDual ∧ i ∈ l.withDualInOther l2
+     ∧ (∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i)) Finset.univ
+
+lemma not_mem_withDual_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
+    i.1 ∉ l.withDual := by
+  have hi := i.2
+  simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach,
+    true_and] at hi
+  exact hi.2.1
+
+lemma mem_withDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
+    i.1 ∈ l.withDualInOther l2 := by
+  have hi := i.2
+  simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach,
+    true_and] at hi
+  exact hi.2.2.1
+
+def fromWithUniqueDualInOther (i : l.withUniqueDualInOther l2) : l.withDualInOther l2 :=
+  ⟨i.1, l.mem_withDualInOther_of_withUniqueDualInOther l2 i⟩
+
+instance : Coe (l.withUniqueDualInOther l2) (l.withDualInOther l2) where
+  coe i := ⟨i.1, l.mem_withDualInOther_of_withUniqueDualInOther l2 i⟩
+
+lemma all_dual_eq_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
+    ∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther! l2 i := by
+  have hi := i.2
+  simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach,
+    true_and] at hi
+  intro j hj
+  refine (Option.get_of_mem _ (hi.2.2.2 j hj).symm).symm
+
+lemma eq_getDualInOther_of_withUniqueDual_iff (i : l.withUniqueDualInOther l2) (j : Fin l2.length) :
+    l.AreDualInOther l2 i j ↔ j = l.getDualInOther! l2 i := by
+  apply Iff.intro
+  intro h
+  exact l.all_dual_eq_of_withUniqueDualInOther l2 i j h
+  intro h
+  subst h
+  exact areDualInOther_getDualInOther! l l2 i
+
+@[simp]
+lemma getDualInOther!_getDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
+    l2.getDualInOther! l (l.getDualInOther l2 i) = i := by
+  by_contra hn
+  refine (l.not_mem_withDual_of_withUniqueDualInOther l2 i)
+    (l.mem_withDual_iff_exists.mpr ⟨(l2.getDualInOther! l (l.getDualInOther l2 i)), ?_⟩ )
+  simp [AreDualInSelf, hn]
+  exact (fun a => hn (id (Eq.symm a)))
+
+@[simp]
+lemma getDualInOther_getDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
+    l2.getDualInOther l (l.getDualInOther l2 i) = i :=
+  SetCoe.ext (getDualInOther!_getDualInOther_of_withUniqueDualInOther l l2 i)
+
+@[simp]
+lemma getDualInOther?_getDualInOther!_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
+    l2.getDualInOther? l (l.getDualInOther! l2 i) = some i := by
+  change l2.getDualInOther? l (l.getDualInOther l2 i) = some i
+  rw [getDualInOther?_eq_some_getDualInOther!]
+  simp
+
+lemma getDualInOther_of_withUniqueDualInOther_not_mem_of_withDual (i : l.withUniqueDualInOther l2) :
+    (l.getDualInOther l2 i).1 ∉ l2.withDual  := by
+  rw [mem_withDual_iff_exists]
+  simp
+  intro j
+  simp [AreDualInSelf]
+  intro hj
+  by_contra hn
+  have hn' : l.AreDualInOther l2 i j  := by
+    simp [AreDualInOther, hn, hj]
+  rw [eq_getDualInOther_of_withUniqueDual_iff] at hn'
+  simp_all
+  simp only [getDualInOther_coe, not_true_eq_false] at hj
+
+lemma getDualInOther_of_withUniqueDualInOther_mem (i : l.withUniqueDualInOther l2) :
+    (l.getDualInOther l2 i).1 ∈ l2.withUniqueDualInOther l := by
+  simp only [withUniqueDualInOther, Finset.mem_filter, Finset.mem_univ, true_and]
+  apply And.intro (l.getDualInOther_of_withUniqueDualInOther_not_mem_of_withDual l2 i)
+  apply And.intro
+  exact Finset.coe_mem
+    (l.getDualInOther l2 ⟨↑i, mem_withDualInOther_of_withUniqueDualInOther l l2 i⟩)
+  intro j hj
+  by_contra hn
+  have h' : l.AreDualInSelf i j := by
+    simp [AreDualInSelf, hn]
+    simp_all [AreDualInOther, getDual]
+    simp [getDualInOther_coe] at hn
+    exact fun a => hn (id (Eq.symm a))
+  have hi := l.not_mem_withDual_of_withUniqueDualInOther l2 i
+  rw [mem_withDual_iff_exists] at hi
+  simp_all
+
+def getDualInOtherEquiv : l.withUniqueDualInOther l2 ≃ l2.withUniqueDualInOther l where
+  toFun x := ⟨l.getDualInOther l2 x, l.getDualInOther_of_withUniqueDualInOther_mem l2 x⟩
+  invFun x := ⟨l2.getDualInOther l x, l2.getDualInOther_of_withUniqueDualInOther_mem l x⟩
+  left_inv x := SetCoe.ext (by simp)
+  right_inv x := SetCoe.ext (by simp)
+
+/-!
+
+## Equality of withUnqiueDual and withDual
+
+-/
+
+lemma withUnqiueDual_eq_withDual_iff_unique_forall :
+    l.withUniqueDual = l.withDual ↔
+    ∀ (i : l.withDual) j, l.AreDualInSelf i j → j = l.getDual? i := by
+  apply Iff.intro
+  · intro h i j hj
+    rw [@Finset.ext_iff] at h
+    simp [withUniqueDual] at h
+    exact h i i.2 j hj
+  · intro h
+    apply Finset.ext
+    intro i
+    apply Iff.intro
+    · intro hi
+      simp [withUniqueDual] at hi
+      exact hi.1
+    · intro hi
+      simp [withUniqueDual]
+      apply And.intro hi
+      intro j hj
+      exact h ⟨i, hi⟩ j hj
+
+
+lemma withUnqiueDual_eq_withDual_iff :
+    l.withUniqueDual = l.withDual ↔
+    ∀ i, (l.getDual? i).bind l.getDual? = Option.guard (fun i => i ∈ l.withDual) i := by
+  apply Iff.intro
+  · intro h i
+    by_cases hi : i ∈ l.withDual
+    · have hii : i ∈ l.withUniqueDual := by
+        simp_all only
+      change (l.getDual? i).bind l.getDual?  = _
+      rw [getDual?_getDual?_of_withUniqueDualInOther l ⟨i, hii⟩]
+      simp
+      symm
+      rw [Option.guard_eq_some]
+      exact ⟨rfl, hi⟩
+    · rw [getDual?_eq_none_on_not_mem l i hi]
+      simp
+      symm
+      simpa only [Option.guard, ite_eq_right_iff, imp_false] using hi
+  · intro h
+    rw [withUnqiueDual_eq_withDual_iff_unique_forall]
+    intro i j hj
+    rcases l.getDual?_of_areDualInSelf hj with hi | hi | hi
+    · have hj' := h j
+      rw [hi] at hj'
+      simp at hj'
+      rw [hj']
+      symm
+      rw [Option.guard_eq_some]
+      exact ⟨rfl, l.mem_withDual_iff_exists.mpr ⟨i, hj.symm⟩⟩
+    · exact hi.symm
+    · have hj' := h j
+      rw [hi] at hj'
+      rw [h i] at hj'
+      have hi : Option.guard (fun i => i ∈ l.withDual) ↑i = some i := by
+         apply Option.guard_eq_some.mpr
+         simp
+      rw [hi] at hj'
+      simp at hj'
+      have hj'' := Option.guard_eq_some.mp hj'.symm
+      have hj''' := hj''.1
+      rw [hj'''] at hj
+      simp at hj
+
+lemma withUnqiueDual_eq_withDual_iff_list_apply :
+    l.withUniqueDual = l.withDual ↔
+    (Fin.list l.length).map (fun i => (l.getDual? i).bind l.getDual?) =
+    (Fin.list l.length).map (fun i => Option.guard (fun i => i ∈ l.withDual) i) := by
+  rw [withUnqiueDual_eq_withDual_iff]
+  apply Iff.intro
+  intro h
+  apply congrFun
+  apply congrArg
+  exact (Set.eqOn_univ (fun i => (l.getDual? i).bind l.getDual?) fun i =>
+    Option.guard (fun i => i ∈ l.withDual) i).mp fun ⦃x⦄ _ => h x
+  intro h
+  intro i
+  simp only [List.map_inj_left] at h
+  have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
+      have h1' : (Fin.list n)[m] = m := Fin.getElem_list _ _
+      exact h1' ▸ List.getElem_mem _ _ _
+  exact h i (h1 i)
+
+def withUnqiueDualEqWithDualBool : Bool :=
+  if (Fin.list l.length).map (fun i => (l.getDual? i).bind l.getDual?) =
+    (Fin.list l.length).map (fun i => Option.guard (fun i => i ∈ l.withDual) i) then
+    true
+  else
+    false
+
+lemma withUnqiueDual_eq_withDual_iff_list_apply_bool :
+    l.withUniqueDual = l.withDual ↔ l.withUnqiueDualEqWithDualBool := by
+  rw [withUnqiueDual_eq_withDual_iff_list_apply]
+  apply Iff.intro
+  intro h
+  simp [withUnqiueDualEqWithDualBool, h]
+  intro h
+  simpa [withUnqiueDualEqWithDualBool] using h
+
+
+
+/-
+
+def withoutDual : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDual? i).isNone) Finset.univ
+
+
+def withoutDualOther : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDualInOther? l2 i).isNone) Finset.univ
+
+lemma withDual_disjoint_withoutDual : Disjoint l.withDual l.withoutDual := by
+  rw [Finset.disjoint_iff_ne]
+  intro a ha b hb
+  by_contra hn
+  subst hn
+  simp_all only [withDual, Finset.mem_filter, Finset.mem_univ, true_and, withoutDual,
+    Option.isNone_iff_eq_none, Option.isSome_none, Bool.false_eq_true]
+
+lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ := by
+  rw [Finset.eq_univ_iff_forall]
+  intro i
+  by_cases h : (l.getDual? i).isSome
+  · simp [withDual, Finset.mem_filter, Finset.mem_univ, h]
+  · simp at h
+    simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h]
+
+lemma withDualOther_disjoint_withoutDualOther :
+    Disjoint (l.withDualOther l2) (l.withoutDualOther l2) := by
+  rw [Finset.disjoint_iff_ne]
+  intro a ha b hb
+  by_contra hn
+  subst hn
+  simp_all only [withDualOther, Finset.mem_filter, Finset.mem_univ, true_and, withoutDualOther,
+    Option.isNone_iff_eq_none, Option.isSome_none, Bool.false_eq_true]
+
+lemma withDualOther_union_withoutDualOther :
+    l.withDualOther l2 ∪ l.withoutDualOther l2 = Finset.univ := by
+  rw [Finset.eq_univ_iff_forall]
+  intro i
+  by_cases h : (l.getDualInOther? l2 i).isSome
+  · simp [withDualOther, Finset.mem_filter, Finset.mem_univ, h]
+  · simp at h
+    simp [withoutDualOther, Finset.mem_filter, Finset.mem_univ, h]
+
+def dualEquiv : l.withDual ⊕ l.withoutDual ≃ Fin l.length :=
+  (Equiv.Finset.union _ _ l.withDual_disjoint_withoutDual).trans <|
+  Equiv.subtypeUnivEquiv (Finset.eq_univ_iff_forall.mp l.withDual_union_withoutDual)
+
+def dualEquivOther : l.withDualOther l2 ⊕ l.withoutDualOther l2 ≃ Fin l.length :=
+  (Equiv.Finset.union _ _ (l.withDualOther_disjoint_withoutDualOther l2)).trans
+  (Equiv.subtypeUnivEquiv
+    (Finset.eq_univ_iff_forall.mp (l.withDualOther_union_withoutDualOther l2)))
+
+/-!
+
 ## Has a dual
 
 -/
 
-def HasDualInSelf (i : Fin l.length) : Prop := ∃ j, AreDualInSelf l i j
+def HasDualInSelf (i : Fin l.length) : Prop := (l.getDual? i).isSome
 
-instance (i : Fin l.length) : Decidable (l.HasDualInSelf i) := Fintype.decidableExistsFintype
+instance (i : Fin l.length) : Decidable (l.HasDualInSelf i) := (l.getDual? i).isSome.decEq true
 
 def HasDualInOther (i : Fin l.length) : Prop :=
   ∃ (j : Fin l2.length), AreDualInOther i j
@@ -107,9 +623,16 @@ namespace HasDualInSelf
 
 variable {l l2 : IndexList X} {i : Fin l.length}
 
+lemma iff_exists : l.HasDualInSelf i ↔ ∃ j, l.AreDualInSelf i j :=
+  Fin.isSome_find_iff
+
+lemma iff_mem : l.HasDualInSelf i ↔ i ∈ l.withDual := by
+  simp [withDual, Finset.mem_filter, Finset.mem_univ, HasDualInSelf]
+
 @[simp]
 lemma append_inl : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i)) ↔
     (l.HasDualInSelf i ∨ l.HasDualInOther l2 i) := by
+  rw [iff_exists, iff_exists]
   apply Iff.intro
   · intro h
     obtain ⟨j, hj⟩ := h
@@ -144,6 +667,7 @@ lemma append_inl : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i)) ↔
 @[simp]
 lemma append_inr {i : Fin l2.length} : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inr i)) ↔
     (l2.HasDualInSelf i ∨ l2.HasDualInOther l i) := by
+  rw [iff_exists, iff_exists]
   apply Iff.intro
   · intro h
     obtain ⟨j, hj⟩ := h
@@ -171,12 +695,6 @@ lemma append_inr {i : Fin l2.length} : (l ++ l2).HasDualInSelf (appendEquiv (Sum
       simp [AreDualInSelf]
       exact hj
 
-def getFirst (h : l.HasDualInSelf i) : Fin l.length :=
-  (Fin.find (l.AreDualInSelf i)).get (by simpa [Fin.isSome_find_iff] using h)
-
-lemma some_getFirst_eq_find  (h : l.HasDualInSelf i)  :
-    Fin.find (l.AreDualInSelf i) = some h.getFirst := by
-  simp [getFirst]
 
 lemma getFirst_hasDualInSelf (h : l.HasDualInSelf i) :
     l.HasDualInSelf h.getFirst := by
@@ -231,7 +749,6 @@ end HasDualInOther
 
 namespace HasDualInSelf
 
-
 @[simp]
 lemma getFirst_append_inl_of_hasDualInSelf (h : (l ++ l2).HasDualInSelf (appendEquiv (Sum.inl i)))
     (hi : l.HasDualInSelf i) : h.getFirst = appendEquiv (Sum.inl hi.getFirst) := by
@@ -409,6 +926,37 @@ lemma get_get (h : l.HasSingDualInSelf i) : h.get_hasSingDualInSelf.get = i := b
 
 /-!
 
+### Bool condition
+
+-/
+
+def bool (l : IndexList X) (i : Fin l.length) : Bool :=
+  if h : l.HasDualInSelf i then
+    let l' := (Fin.list l.length).filterMap fun j => if l.AreDualInSelf j i ∧ j ≠ h.getFirst
+      then some j else none
+    List.isEmpty l'
+  else false
+
+lemma of_bool_true (h : bool l i) : l.HasSingDualInSelf i := by
+  simp [bool] at h
+  split at h <;> rename_i h1
+  · rw [List.isEmpty_iff_eq_nil] at h
+    rw [List.filterMap_eq_nil] at h
+    simp at h
+    apply And.intro h1
+    intro h' j
+    have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
+      have h1' : (Fin.list n)[m] = m := by
+        erw [Fin.getElem_list]
+        rfl
+      rw [← h1']
+      apply List.getElem_mem
+    intro h2
+    exact h j (h1 j) h2.symm
+  · exact False.elim h
+
+/-!
+
 ### Relations regarding append for HasSingDualInSelf
 
 -/
@@ -810,6 +1358,9 @@ end HasSingColorDualInSelf
 
 def HasSingColorDualsInSelf : Prop := ∀ i, l.HasSingColorDualInSelf i ∨ ¬ l.HasDualInSelf i
 
+def HasSingColorDualsInOther : Prop := ∀ i, l.HasSingColorDualInOther l2 i
+  ∨ ¬ l.HasDualInOther l2 i
+
 namespace HasSingColorDualsInSelf
 
 variable {l : IndexList 𝓒.Color}
@@ -829,12 +1380,12 @@ lemma _root_.IndexNotation.IndexList.HasNoDualsSelf.toHasSingColorDualsInSelf
   fun i => Or.inr (h i)
 
 end HasSingColorDualsInSelf
-def HasSingColorDualsInOther : Prop := ∀ i, l.HasSingColorDualInOther l2 i ∨ ¬ l.HasDualInOther l2 i
+
 
 
 end Color
 
-
+-/
 end IndexList
 
 end IndexNotation
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean
index fe6ff6a..8b4c7e5 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean
@@ -18,35 +18,106 @@ namespace IndexList
 variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
 variable (l l2 : IndexList X)
 
+def getDual? (i : Fin l.length) : Option (Fin l.length) :=
+  Fin.find (fun j => i ≠ j ∧ l.idMap i = l.idMap j)
 
-def getDual (i : Fin l.length) : Option (Fin l.length) :=
-  if h : l.HasDualInSelf i then
-    some h.getFirst
-  else
-    none
+def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) :=
+  Fin.find (fun j => l.idMap i = l2.idMap j)
 
-lemma getDual_of_hasDualInSelf {i : Fin l.length} (h : l.HasDualInSelf i) :
-    l.getDual i = some h.getFirst := by
-  simp [getDual, h]
+/-!
 
-lemma getDual_of_not_hasDualInSelf {i : Fin l.length} (h :  ¬l.HasDualInSelf i) :
-    l.getDual i = none := by
-  simp [getDual, h]
+## Finite sets of duals
 
-def getDualOther (i : Fin l.length) : Option (Fin l2.length) :=
-  if h : l.HasDualInOther l2 i then
-    some h.getFirst
-  else
-    none
+-/
 
-lemma getDualOther_of_hasDualInOther {i : Fin l.length} (h : l.HasDualInOther l2 i) :
-    l.getDualOther l2 i = some h.getFirst := by
-  simp [getDualOther, h]
+def withDual : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDual? i).isSome) Finset.univ
 
-lemma getDualOther_of_not_hasDualInOther {i : Fin l.length} (h :  ¬l.HasDualInOther l2 i) :
-    l.getDualOther l2 i = none := by
-  simp [getDualOther, h]
+def withoutDual : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDual? i).isNone) Finset.univ
 
+def withDualOther : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDualInOther? l2 i).isSome) Finset.univ
+
+def withoutDualOther : Finset (Fin l.length) :=
+  Finset.filter (fun i => (l.getDualInOther? l2 i).isNone) Finset.univ
+
+lemma withDual_disjoint_withoutDual : Disjoint l.withDual l.withoutDual := by
+  rw [Finset.disjoint_iff_ne]
+  intro a ha b hb
+  by_contra hn
+  subst hn
+  simp_all only [withDual, Finset.mem_filter, Finset.mem_univ, true_and, withoutDual,
+    Option.isNone_iff_eq_none, Option.isSome_none, Bool.false_eq_true]
+
+lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ := by
+  rw [Finset.eq_univ_iff_forall]
+  intro i
+  by_cases h : (l.getDual? i).isSome
+  · simp [withDual, Finset.mem_filter, Finset.mem_univ, h]
+  · simp at h
+    simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h]
+
+lemma withDualOther_disjoint_withoutDualOther :
+    Disjoint (l.withDualOther l2) (l.withoutDualOther l2) := by
+  rw [Finset.disjoint_iff_ne]
+  intro a ha b hb
+  by_contra hn
+  subst hn
+  simp_all only [withDualOther, Finset.mem_filter, Finset.mem_univ, true_and, withoutDualOther,
+    Option.isNone_iff_eq_none, Option.isSome_none, Bool.false_eq_true]
+
+lemma withDualOther_union_withoutDualOther :
+    l.withDualOther l2 ∪ l.withoutDualOther l2 = Finset.univ := by
+  rw [Finset.eq_univ_iff_forall]
+  intro i
+  by_cases h : (l.getDualInOther? l2 i).isSome
+  · simp [withDualOther, Finset.mem_filter, Finset.mem_univ, h]
+  · simp at h
+    simp [withoutDualOther, Finset.mem_filter, Finset.mem_univ, h]
+
+def dualEquiv : l.withDual ⊕ l.withoutDual ≃ Fin l.length :=
+  (Equiv.Finset.union _ _ l.withDual_disjoint_withoutDual).trans <|
+  Equiv.subtypeUnivEquiv (Finset.eq_univ_iff_forall.mp l.withDual_union_withoutDual)
+
+def dualEquivOther : l.withDualOther l2 ⊕ l.withoutDualOther l2 ≃ Fin l.length :=
+  (Equiv.Finset.union _ _ (l.withDualOther_disjoint_withoutDualOther l2)).trans
+  (Equiv.subtypeUnivEquiv
+    (Finset.eq_univ_iff_forall.mp (l.withDualOther_union_withoutDualOther l2)))
+
+/-!
+
+## Index lists where `getDual?` is invertiable.
+-/
+
+def InverDual : Prop :=
+  ∀ i, (l.getDual? i).bind l.getDual? = some i
+
+namespace InverDual
+
+end InverDual
+
+def InvertDualOther : Prop :=
+  ∀ i, (l.getDualInOther? l2 i).bind (l2.getDualInOther? l) = some i
+  ∧ ∀ i, (l2.getDualInOther? l i).bind (l.getDualInOther? l2) = some i
+
+section Color
+
+variable {𝓒 : TensorColor}
+variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
+variable (l l2 : IndexList 𝓒.Color)
+/-!
+
+## Has single dual of correct color
+
+-/
+
+def IndexListColor (𝓒 : TensorColor) [IndexNotation 𝓒.Color] : Type := {l : IndexList X //
+  ∀ i, (l.getDual? i).bind l.getDual? = some i ∧
+  Option.map (l.colorMap) ∘ l.getDual? = Option.map ()
+  }
+
+end color
 /-!
 
 ## Append relations
@@ -104,10 +175,42 @@ def HasSingDualsInOther : Prop :=
 
 def HasNoDualsInSelf : Prop := l.getDual = fun _ => none
 
-lemma hasSingDualsInSelf_append :
-    (l ++ l2).HasSingDualsInSelf ↔
-    l.HasSingDualsInSelf ∧ l2.HasSingDualsInSelf ∧ HasSingDualsInOther l1 l2 := by
-  sorry
+lemma hasSingDualsInSelf_append (h1 : l.HasNoDualsInSelf) (h2 : l2.HasNoDualsInSelf) :
+    (l ++ l2).HasSingDualsInSelf ↔ HasSingDualsInOther l l2 := by
+  apply Iff.intro
+  · intro h
+    simp [HasSingDualsInOther]
+    apply And.intro
+    · intro i
+      have h3 := h (appendEquiv (Sum.inl i))
+      simp at h3
+      rw [h1] at h3
+      simp at h3
+      by_cases hn : l.HasDualInOther l2 i
+      · rw [l.getDualOther_of_hasDualInOther l2 hn] at h3 ⊢
+        simp only [Option.map_some', Function.comp_apply, Option.some_bind, getDual_append_inr] at h3
+        rw [h2] at h3
+        simpa using h3
+      · rw [l.getDualOther_of_not_hasDualInOther l2 hn] at h3 ⊢
+        simp at h3
+    · intro i
+      have h3 := h (appendEquiv (Sum.inr i))
+      simp at h3
+      rw [h2] at h3
+      simp at h3
+      by_cases hn : l2.HasDualInOther l i
+      · rw [l2.getDualOther_of_hasDualInOther l hn] at h3 ⊢
+        simp only [Option.map_some', Function.comp_apply, Option.some_bind, getDual_append_inl] at h3
+        rw [h1] at h3
+        simpa using h3
+      · rw [l2.getDualOther_of_not_hasDualInOther l hn] at h3 ⊢
+        simp at h3
+  · intro h
+    intro i
+    obtain ⟨k, hk⟩ := appendEquiv.surjective i
+
+    sorry
+
 end IndexList
 
 end IndexNotation