diff --git a/HepLean.lean b/HepLean.lean
index f041b4d..47bb429 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -120,7 +120,7 @@ import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
 import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
 import HepLean.PerturbationTheory.FieldStatistics
 import HepLean.PerturbationTheory.Wick.Contractions
-import HepLean.PerturbationTheory.Wick.CreateAnnilateSection
+import HepLean.PerturbationTheory.Wick.CreateAnnihilateSection
 import HepLean.PerturbationTheory.Wick.KoszulOrder
 import HepLean.PerturbationTheory.Wick.OfList
 import HepLean.PerturbationTheory.Wick.OperatorMap
diff --git a/HepLean/PerturbationTheory/Wick/Contractions.lean b/HepLean/PerturbationTheory/Wick/Contractions.lean
index f579031..dadb339 100644
--- a/HepLean/PerturbationTheory/Wick/Contractions.lean
+++ b/HepLean/PerturbationTheory/Wick/Contractions.lean
@@ -172,7 +172,7 @@ lemma toCenterTerm_center (f : 𝓕 → Type) [∀ i, Fintype (f i)]
     rw [map_sum, map_sum]
     refine Subalgebra.sum_mem (Subalgebra.center ℂ A) ?hy.hx.h
     intro x _
-    simp only [CreateAnnilateSect.toList]
+    simp only [CreateAnnihilateSect.toList]
     rw [ofList_singleton]
     exact OperatorMap.superCommute_ofList_singleton_ι_center (q := fun i => q i.1)
       (le1 := le1) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
diff --git a/HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean b/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean
similarity index 88%
rename from HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean
rename to HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean
index 0106fcb..e0bce43 100644
--- a/HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean
+++ b/HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean
@@ -19,35 +19,35 @@ open FieldStatistic
   each field as a `creation` or an `annilation` operator. E.g. the number of terms
   `φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
   operators at this point (e.g. ansymptotic states) this is accounted for. -/
-def CreateAnnilateSect {𝓕 : Type} (f : 𝓕 → Type) (l : List 𝓕) : Type :=
+def CreateAnnihilateSect {𝓕 : Type} (f : 𝓕 → Type) (l : List 𝓕) : Type :=
   Π i, f (l.get i)
 
-namespace CreateAnnilateSect
+namespace CreateAnnihilateSect
 
 section basic_defs
 
-variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {l : List 𝓕} (a : CreateAnnilateSect f l)
+variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {l : List 𝓕} (a : CreateAnnihilateSect f l)
 
-/-- The type `CreateAnnilateSect f l` is finite. -/
-instance fintype : Fintype (CreateAnnilateSect f l) := Pi.fintype
+/-- The type `CreateAnnihilateSect f l` is finite. -/
+instance fintype : Fintype (CreateAnnihilateSect f l) := Pi.fintype
 
 /-- The section got by dropping the first element of `l` if it exists. -/
-def tail : {l : List 𝓕} → (a : CreateAnnilateSect f l) → CreateAnnilateSect f l.tail
+def tail : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → CreateAnnihilateSect f l.tail
   | [], a => a
   | _ :: _, a => fun i => a (Fin.succ i)
 
 /-- For a list of fields `i :: l` the value of the section at the head `i`. -/
-def head {i : 𝓕} (a : CreateAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
+def head {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
 
 end basic_defs
 
 section toList_basic
 
 variable {𝓕 : Type} {f : 𝓕 → Type} (q : 𝓕 → FieldStatistic)
-  {l : List 𝓕} (a : CreateAnnilateSect f l)
+  {l : List 𝓕} (a : CreateAnnihilateSect f l)
 
 /-- The list `List (Σ i, f i)` defined by `a`. -/
-def toList : {l : List 𝓕} → (a : CreateAnnilateSect f l) → List (Σ i, f i)
+def toList : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → List (Σ i, f i)
   | [], _ => []
   | i :: _, a => ⟨i, a.head⟩ :: toList a.tail
 
@@ -59,16 +59,16 @@ lemma toList_length : (toList a).length = l.length := by
     simp only [toList, List.length_cons, Fin.zero_eta]
     rw [ih]
 
-lemma toList_tail : {l : List 𝓕} → (a : CreateAnnilateSect f l) → toList a.tail = (toList a).tail
+lemma toList_tail : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → toList a.tail = (toList a).tail
   | [], _ => rfl
   | i :: l, a => by
     simp [toList]
 
-lemma toList_cons {i : 𝓕} (a : CreateAnnilateSect f (i :: l)) :
+lemma toList_cons {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) :
     (toList a) = ⟨i, a.head⟩ :: toList a.tail := by
   rfl
 
-lemma toList_get (a : CreateAnnilateSect f l) :
+lemma toList_get (a : CreateAnnihilateSect f l) :
     (toList a).get = (fun i => ⟨l.get i, a i⟩) ∘ Fin.cast (by simp) := by
   induction l with
   | nil =>
@@ -108,7 +108,7 @@ lemma toList_grade :
 
 @[simp]
 lemma toList_grade_take (q : 𝓕 → FieldStatistic) :
-    (r : List 𝓕) → (a : CreateAnnilateSect f r) → (n : ℕ) →
+    (r : List 𝓕) → (a : CreateAnnihilateSect f r) → (n : ℕ) →
     ofList (fun i => q i.fst) (List.take n a.toList) = ofList q (List.take n r)
   | [], _, _ => by
     simp [toList]
@@ -124,15 +124,15 @@ section toList_erase
 
 variable {𝓕 : Type} {f : 𝓕 → Type} {l : List 𝓕}
 
-/-- The equivalence between `CreateAnnilateSect f l` and
-  `f (l.get n) × CreateAnnilateSect f (l.eraseIdx n)` obtained by extracting the `n`th field
+/-- The equivalence between `CreateAnnihilateSect f l` and
+  `f (l.get n) × CreateAnnihilateSect f (l.eraseIdx n)` obtained by extracting the `n`th field
   from `l`. -/
-def extractEquiv (n : Fin l.length) : CreateAnnilateSect f l ≃
-    f (l.get n) × CreateAnnilateSect f (l.eraseIdx n) := by
+def extractEquiv (n : Fin l.length) : CreateAnnihilateSect f l ≃
+    f (l.get n) × CreateAnnihilateSect f (l.eraseIdx n) := by
   match l with
   | [] => exact Fin.elim0 n
   | l0 :: l =>
-    let e1 : CreateAnnilateSect f ((l0 :: l).eraseIdx n) ≃ Π i, f ((l0 :: l).get (n.succAbove i)) :=
+    let e1 : CreateAnnihilateSect f ((l0 :: l).eraseIdx n) ≃ Π i, f ((l0 :: l).get (n.succAbove i)) :=
       Equiv.piCongr (Fin.castOrderIso (by rw [eraseIdx_cons_length])).toEquiv
       fun x => Equiv.cast (congrArg f (by
       rw [HepLean.List.eraseIdx_get]
@@ -162,15 +162,15 @@ def extractEquiv (n : Fin l.length) : CreateAnnilateSect f l ≃
     exact (Fin.insertNthEquiv _ _).symm.trans (Equiv.prodCongr (Equiv.refl _) e1.symm)
 
 lemma extractEquiv_symm_toList_get_same (n : Fin l.length) (a0 : f (l.get n))
-    (a : CreateAnnilateSect f (l.eraseIdx n)) :
+    (a : CreateAnnihilateSect f (l.eraseIdx n)) :
     ((extractEquiv n).symm (a0, a)).toList[n] = ⟨l[n], a0⟩ := by
   match l with
   | [] => exact Fin.elim0 n
   | l0 :: l =>
-    trans (((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
+    trans (((CreateAnnihilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
     · simp only [List.length_cons, List.get_eq_getElem, Fin.coe_cast]
       rfl
-    rw [CreateAnnilateSect.toList_get]
+    rw [CreateAnnihilateSect.toList_get]
     simp only [List.get_eq_getElem, List.length_cons, extractEquiv, RelIso.coe_fn_toEquiv,
       Fin.castOrderIso_apply, Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.prodCongr_symm,
       Equiv.refl_symm, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_apply, id_eq,
@@ -181,12 +181,12 @@ lemma extractEquiv_symm_toList_get_same (n : Fin l.length) (a0 : f (l.get n))
     simp only [Fin.insertNth_apply_same]
 
 /-- The section obtained by dropping the `n`th field. -/
-def eraseIdx (a : CreateAnnilateSect f l) (n : Fin l.length) :
-    CreateAnnilateSect f (l.eraseIdx n) :=
+def eraseIdx (a : CreateAnnihilateSect f l) (n : Fin l.length) :
+    CreateAnnihilateSect f (l.eraseIdx n) :=
   (extractEquiv n a).2
 
 @[simp]
-lemma eraseIdx_zero_tail {i : 𝓕} (a : CreateAnnilateSect f (i :: l)) :
+lemma eraseIdx_zero_tail {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) :
     (eraseIdx a (@OfNat.ofNat (Fin (l.length + 1)) 0 Fin.instOfNat : Fin (l.length + 1))) =
     a.tail := by
   simp only [List.length_cons, Fin.val_zero, List.eraseIdx_cons_zero, eraseIdx, List.get_eq_getElem,
@@ -196,7 +196,7 @@ lemma eraseIdx_zero_tail {i : 𝓕} (a : CreateAnnilateSect f (i :: l)) :
   rfl
 
 lemma eraseIdx_succ_head {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
-    (a : CreateAnnilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
+    (a : CreateAnnihilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
   rw [eraseIdx, extractEquiv]
   simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, List.eraseIdx_cons_succ,
     RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply, Equiv.prodCongr_apply,
@@ -217,7 +217,7 @@ lemma eraseIdx_succ_head {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
   simp [Fin.ext_iff]
 
 lemma eraseIdx_succ_tail {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
-    (a : CreateAnnilateSect f (i :: l)) :
+    (a : CreateAnnihilateSect f (i :: l)) :
     (eraseIdx a ⟨n + 1, hn⟩).tail = eraseIdx a.tail ⟨n, Nat.succ_lt_succ_iff.mp hn⟩ := by
   match l with
   | [] =>
@@ -278,7 +278,7 @@ lemma eraseIdx_succ_tail {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
       omega
     next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]
 
-lemma eraseIdx_toList : {l : List 𝓕} → {n : Fin l.length} → (a : CreateAnnilateSect f l) →
+lemma eraseIdx_toList : {l : List 𝓕} → {n : Fin l.length} → (a : CreateAnnihilateSect f l) →
     (eraseIdx a n).toList = a.toList.eraseIdx n
   | [], n, _ => Fin.elim0 n
   | r0 :: r, ⟨0, h⟩, a => by
@@ -292,7 +292,7 @@ lemma eraseIdx_toList : {l : List 𝓕} → {n : Fin l.length} → (a : CreateAn
       rw [eraseIdx_succ_tail]
 
 lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type}
-    {l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreateAnnilateSect f (l.eraseIdx n)) :
+    {l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreateAnnihilateSect f (l.eraseIdx n)) :
     ((extractEquiv n).symm (a0, a)).eraseIdx n = a := by
   match l with
   | [] => exact Fin.elim0 n
@@ -305,7 +305,7 @@ end toList_erase
 section toList_sign_conditions
 
 variable {𝓕 : Type} {f : 𝓕 → Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
-  {l : List 𝓕} (a : CreateAnnilateSect f l)
+  {l : List 𝓕} (a : CreateAnnihilateSect f l)
 
 lemma toList_koszulSignInsert (x : (i : 𝓕) × f i) :
     koszulSignInsert (fun i => q i.fst) (fun i j => le i.fst j.fst) x a.toList =
@@ -379,7 +379,7 @@ lemma insertionSortEquiv_toList :
     have h3 : (List.insertionSort le (List.map (fun i => i.1) a.tail.toList)) =
       List.insertionSort le l := by
       congr
-      have h3' (l : List 𝓕) (a : CreateAnnilateSect f l) :
+      have h3' (l : List 𝓕) (a : CreateAnnihilateSect f l) :
         List.map (fun i => i.1) a.toList = l := by
         induction l with
         | nil => rfl
@@ -397,7 +397,7 @@ lemma insertionSortEquiv_toList :
 /-- Given a section for `l` the corresponding section
   for `List.insertionSort le1 l`. -/
 def sort :
-    CreateAnnilateSect f (List.insertionSort le l) :=
+    CreateAnnihilateSect f (List.insertionSort le l) :=
   Equiv.piCongr (HepLean.List.insertionSortEquiv le l) (fun i => (Equiv.cast (by
       congr 1
       rw [← HepLean.List.insertionSortEquiv_get]
@@ -432,6 +432,6 @@ lemma sort_toList :
   simp
 
 end toList_sign_conditions
-end CreateAnnilateSect
+end CreateAnnihilateSect
 
 end Wick
diff --git a/HepLean/PerturbationTheory/Wick/OfList.lean b/HepLean/PerturbationTheory/Wick/OfList.lean
index 7b7c9e8..674ae10 100644
--- a/HepLean/PerturbationTheory/Wick/OfList.lean
+++ b/HepLean/PerturbationTheory/Wick/OfList.lean
@@ -3,7 +3,7 @@ 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.PerturbationTheory.Wick.CreateAnnilateSection
+import HepLean.PerturbationTheory.Wick.CreateAnnihilateSection
 import HepLean.PerturbationTheory.Wick.KoszulOrder
 /-!
 
@@ -142,15 +142,15 @@ lemma ofListLift_cons_eq_ofListLift (f : 𝓕 → Type) [∀ i, Fintype (f i)] (
   simp only [one_smul]
 
 lemma ofListLift_expand (f : 𝓕 → Type) [∀ i, Fintype (f i)] (x : ℂ) :
-    (l : List 𝓕) → ofListLift f l x = ∑ (a : CreateAnnilateSect f l), ofList a.toList x
+    (l : List 𝓕) → ofListLift f l x = ∑ (a : CreateAnnihilateSect f l), ofList a.toList x
   | [] => by
-    simp only [ofListLift, CreateAnnilateSect, List.length_nil, List.get_eq_getElem,
-      Finset.univ_unique, CreateAnnilateSect.toList, Finset.sum_const, Finset.card_singleton,
+    simp only [ofListLift, CreateAnnihilateSect, List.length_nil, List.get_eq_getElem,
+      Finset.univ_unique, CreateAnnihilateSect.toList, Finset.sum_const, Finset.card_singleton,
       one_smul]
     rw [ofList_eq_smul_one, map_smul, ofList_empty, ofList_eq_smul_one, ofList_empty, map_one]
   | i :: l => by
     rw [ofListLift_cons, ofListLift_expand f x l]
-    conv_rhs => rw [← (CreateAnnilateSect.extractEquiv
+    conv_rhs => rw [← (CreateAnnihilateSect.extractEquiv
         ⟨0, by exact Nat.zero_lt_succ l.length⟩).symm.sum_comp (α := FreeAlgebra ℂ _)]
     erw [Finset.sum_product]
     rw [Finset.sum_mul]
@@ -178,13 +178,13 @@ lemma koszulOrder_ofListLift {f : 𝓕 → Type} [∀ i, Fintype (f i)]
     rhs
     intro a
     rw [koszulOrder_ofList]
-    rw [CreateAnnilateSect.toList_koszulSign]
+    rw [CreateAnnihilateSect.toList_koszulSign]
   rw [← Finset.smul_sum]
   apply congrArg
   conv_lhs =>
     rhs
     intro n
-    rw [← CreateAnnilateSect.sort_toList]
+    rw [← CreateAnnihilateSect.sort_toList]
   rw [ofListLift_expand]
   refine Fintype.sum_equiv
     ((HepLean.List.insertionSortEquiv le l).piCongr fun i => Equiv.cast ?_) _ _ ?_
diff --git a/HepLean/PerturbationTheory/Wick/OperatorMap.lean b/HepLean/PerturbationTheory/Wick/OperatorMap.lean
index 60805e3..6db2a0b 100644
--- a/HepLean/PerturbationTheory/Wick/OperatorMap.lean
+++ b/HepLean/PerturbationTheory/Wick/OperatorMap.lean
@@ -276,9 +276,9 @@ lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀
     rw [ofList_singleton, koszulOrder_ι]
   | r0 :: r =>
   rw [ofListLift_expand, map_sum, Finset.mul_sum, map_sum]
-  let e1 (a : CreateAnnilateSect f (r0 :: r)) :
+  let e1 (a : CreateAnnihilateSect f (r0 :: r)) :
         Option (Fin a.toList.length) ≃ Option (Fin (r0 :: r).length) :=
-      Equiv.optionCongr (Fin.castOrderIso (CreateAnnilateSect.toList_length a)).toEquiv
+      Equiv.optionCongr (Fin.castOrderIso (CreateAnnihilateSect.toList_length a)).toEquiv
   conv_lhs =>
     rhs
     intro a
@@ -300,25 +300,25 @@ lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀
     rw [ofList_cons_eq_ofList]
   · congr
     funext n
-    rw [← (CreateAnnilateSect.extractEquiv n).symm.sum_comp]
+    rw [← (CreateAnnihilateSect.extractEquiv n).symm.sum_comp]
     simp only [List.get_eq_getElem, List.length_cons, Equiv.optionCongr_symm, OrderIso.toEquiv_symm,
       Fin.symm_castOrderIso, Equiv.optionCongr_apply, RelIso.coe_fn_toEquiv, Option.map_some',
       Fin.castOrderIso_apply, Algebra.smul_mul_assoc, e1]
     erw [Finset.sum_product]
-    have h1 (a0 : f (r0 :: r)[↑n]) (a : CreateAnnilateSect f ((r0 :: r).eraseIdx ↑n)) :
+    have h1 (a0 : f (r0 :: r)[↑n]) (a : CreateAnnihilateSect f ((r0 :: r).eraseIdx ↑n)) :
       superCommuteCenterOrder (fun i => q i.fst)
-        ((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList i F
+        ((CreateAnnihilateSect.extractEquiv n).symm (a0, a)).toList i F
       (some (Fin.cast (by simp) n)) =
       superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) (r0 :: r)) •
       F (((superCommute fun i => q i.fst) (ofList [i] 1))
       (FreeAlgebra.ι ℂ ⟨(r0 :: r).get n, a0⟩)) := by
       simp only [superCommuteCenterOrder, List.get_eq_getElem, List.length_cons, Fin.coe_cast]
-      erw [CreateAnnilateSect.extractEquiv_symm_toList_get_same]
+      erw [CreateAnnihilateSect.extractEquiv_symm_toList_get_same]
       have hsc : superCommuteCoef (fun i => q i.fst) [⟨(r0 :: r).get n, a0⟩]
-        (List.take (↑n) ((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList) =
+        (List.take (↑n) ((CreateAnnihilateSect.extractEquiv n).symm (a0, a)).toList) =
         superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) ((r0 :: r))) := by
         simp only [superCommuteCoef, List.get_eq_getElem, List.length_cons, Fin.isValue,
-          CreateAnnilateSect.toList_grade_take]
+          CreateAnnihilateSect.toList_grade_take]
         rfl
       erw [hsc]
       rfl
@@ -340,8 +340,8 @@ lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀
       intro a
       simp [optionEraseZ]
       enter [2, 2, 1]
-      rw [← CreateAnnilateSect.eraseIdx_toList]
-      erw [CreateAnnilateSect.extractEquiv_symm_eraseIdx]
+      rw [← CreateAnnihilateSect.eraseIdx_toList]
+      erw [CreateAnnihilateSect.extractEquiv_symm_eraseIdx]
     rw [← Finset.sum_mul]
     conv_lhs =>
       lhs
diff --git a/HepLean/PerturbationTheory/Wick/StaticTheorem.lean b/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
index 8f71c1c..a47f7d7 100644
--- a/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
+++ b/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
@@ -17,34 +17,31 @@ noncomputable section
 open HepLean.List
 open FieldStatistic
 
-lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → FieldStatistic)
-    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
-    {A : Type} [Semiring A] [Algebra ℂ A]
+variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] (q : 𝓕 → FieldStatistic)
+  (le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
+
+lemma static_wick_nil {A : Type} [Semiring A] [Algebra ℂ A]
     (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A)
-    (S : Contractions.Splitting f le1) :
+    (S : Contractions.Splitting f le) :
     F (ofListLift f [] 1) = ∑ c : Contractions [],
-    c.toCenterTerm f q le1 F S *
-    F (koszulOrder (fun i => q i.fst) le1 (ofListLift f c.normalize 1)) := by
+    c.toCenterTerm f q le F S *
+    F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
   rw [← Contractions.nilEquiv.symm.sum_comp]
   simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
     Finset.sum_const, Finset.card_singleton, one_smul]
   dsimp [Contractions.normalize, Contractions.toCenterTerm]
   simp [ofListLift_empty]
 
-lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → FieldStatistic)
-    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
-    [IsTrans ((i : I) × f i) le1] [IsTotal ((i : I) × f i) le1]
-    {A : Type} [Semiring A] [Algebra ℂ A] (r : List I) (a : I)
-    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
-    (S : Contractions.Splitting f le1)
+lemma static_wick_cons [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]
+    {A : Type} [Semiring A] [Algebra ℂ A] (r : List 𝓕) (a : 𝓕)
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F]
+    (S : Contractions.Splitting f le)
     (ih : F (ofListLift f r 1) =
-    ∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder (fun i => q i.fst) le1
+    ∑ c : Contractions r, c.toCenterTerm f q le F S * F (koszulOrder (fun i => q i.fst) le
       (ofListLift f c.normalize 1))) :
     F (ofListLift f (a :: r) 1) = ∑ c : Contractions (a :: r),
-      c.toCenterTerm f q le1 F S *
-      F (koszulOrder (fun i => q i.fst) le1 (ofListLift f c.normalize 1)) := by
+      c.toCenterTerm f q le F S *
+      F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
   rw [ofListLift_cons_eq_ofListLift, map_mul, ih, Finset.mul_sum,
     ← Contractions.consEquiv.symm.sum_comp]
   erw [Finset.sum_sigma]
@@ -52,7 +49,7 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
   funext c
   have hb := S.h𝓑 a
   rw [← mul_assoc]
-  have hi := c.toCenterTerm_center f q le1 F S
+  have hi := c.toCenterTerm_center f q le F S
   rw [Subalgebra.mem_center_iff] at hi
   rw [hi, mul_assoc, ← map_mul, hb, add_mul, map_add]
   conv_lhs =>
@@ -86,18 +83,15 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
   exact S.h𝓑p a
   exact S.h𝓑n a
 
-theorem static_wick_theorem {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → FieldStatistic)
-    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] [IsTrans ((i : I) × f i) le1]
-    [IsTotal ((i : I) × f i) le1]
-    {A : Type} [Semiring A] [Algebra ℂ A] (r : List I)
-    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
-    (S : Contractions.Splitting f le1) :
-    F (ofListLift f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le1 F S *
-    F (koszulOrder (fun i => q i.fst) le1 (ofListLift f c.normalize 1)) := by
+theorem static_wick_theorem [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]
+    {A : Type} [Semiring A] [Algebra ℂ A] (r : List 𝓕)
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F]
+    (S : Contractions.Splitting f le) :
+    F (ofListLift f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le F S *
+    F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
   induction r with
-  | nil => exact static_wick_nil q le1 F S
-  | cons a r ih => exact static_wick_cons q le1 r a F S ih
+  | nil => exact static_wick_nil q le F S
+  | cons a r ih => exact static_wick_cons q le r a F S ih
 
 end
 end Wick
diff --git a/HepLean/PerturbationTheory/Wick/SuperCommute.lean b/HepLean/PerturbationTheory/Wick/SuperCommute.lean
index f290fbf..1cae785 100644
--- a/HepLean/PerturbationTheory/Wick/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Wick/SuperCommute.lean
@@ -396,7 +396,7 @@ lemma superCommute_ofList_ofListLift_cons (l : List (Σ i, f i)) (r : List 𝓕)
     rw [ofListLift_expand]
     rw [Finset.mul_sum]
   rw [map_sum]
-  trans ∑ (n : CreateAnnilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
+  trans ∑ (n : CreateAnnihilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
     ((FreeAlgebra.ι ℂ ⟨b1, j⟩) * ofList n.toList y)
   · apply congrArg
     funext n