∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)},
  (∀ ⦃a a' : α⦄ ⦃b b' : β⦄ ⦃c c' : γ⦄, (a', b, c) ∈ t → (a, b', c) ∈ t → (a, b, c') ∈ t → a = a' ∨ b = b' ∨ c = c') →
    SimpleGraph.TripartiteFromTriangles.NoAccidental t