Time Contract mem center

lemma timeContract_mem_center (φ ψ : 𝓕.FieldOp) :    timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra := by  by_cases h : timeOrderRel φ ψ  · rw [timeContract_of_timeOrderRel _ _ h]    exact superCommute_anPart_ofFieldOp_mem_center φ ψ  · rw [timeContract_of_not_timeOrderRel _ _ h]    refine Subalgebra.smul_mem (Subalgebra.center ℂ _) ?_ 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ)    rw [timeContract_of_timeOrderRel]    exact superCommute_anPart_ofFieldOp_mem_center _ _    have h1 := Std.Total.total (r := 𝓕.timeOrderRel) φ ψ    simp_all