Time Order of Field Op List eq Time Only

lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.FieldOp) :    𝓣(ofFieldOpList φs) = ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs)}),    φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by  rw [static_wick_theorem φs]  let e2 : WickContraction φs.length ≃    {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} ⊕    {φsΛ : WickContraction φs.length // ¬ φsΛ.EqTimeOnly} :=    (Equiv.sumCompl _).symm  rw [← e2.symm.sum_comp]  simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type,    Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, map_add, map_sum, e2]  simp only [staticWickTerm, Algebra.smul_mul_assoc, map_smul]  conv_lhs =>    enter [2, 2, x]    rw [timeOrder_timeOrder_left, timeOrder_staticContract_of_not_mem _ x.2]  simp only [zero_mul, map_zero, smul_zero, Finset.sum_const_zero, add_zero]  congr  funext x  rw [staticContract_eq_timeContract_of_eqTimeOnly,    timeOrder_timeContract_mul_of_eqTimeOnly_left] <;>    exact x.2