Specific associativity results for tensor trees

theorem TensorTree.assoc_one_two_two {S : TensorSpecies} {c1 c2 c3 : S.C} (t1 : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (t2 : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) (t3 : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c2, c3])).V) : (contr 0 0 ⋯ ((contr 0 0 ⋯ ((tensorNode t1).prod (tensorNode t2))).prod (tensorNode t3))).tensor = (perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 1)) ⋯) (contr 0 0 ⋯ ((tensorNode t1).prod (contr 1 1 ⋯ ((tensorNode t2).prod (tensorNode t3)))))).tensor

The associativity lemma for t1 | μ ⊗ t2 | μ ν ⊗ t3 | ν σ.