∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)}
  {motive : (a a_1 : α ⊕ β ⊕ γ) → SimpleGraph.TripartiteFromTriangles.Rel t a a_1 → Prop} {a a_1 : α ⊕ β ⊕ γ}
  (t_1 : SimpleGraph.TripartiteFromTriangles.Rel t a a_1),
  (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₀ a) (Sum3.in₁ b) ⋯) →
    (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₁ b) (Sum3.in₀ a) ⋯) →
      (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₀ a) (Sum3.in₂ c) ⋯) →
        (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₂ c) (Sum3.in₀ a) ⋯) →
          (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₁ b) (Sum3.in₂ c) ⋯) →
            (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ (a_2 : (a, b, c) ∈ t), motive (Sum3.in₂ c) (Sum3.in₁ b) ⋯) → motive a a_1 t_1