∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ X₃ X₄ : C} {f₁₂ : X₁ ⟶ X₂} {f₁₃ : X₁ ⟶ X₃}
  {f₂₄ : X₂ ⟶ X₄} {f₃₄ : X₃ ⟶ X₄}
  {fac : CategoryTheory.CategoryStruct.comp f₁₂ f₂₄ = CategoryTheory.CategoryStruct.comp f₁₃ f₃₄}
  {X₁_1 X₂_1 X₃_1 X₄_1 : C} {f₁₂_1 : X₁_1 ⟶ X₂_1} {f₁₃_1 : X₁_1 ⟶ X₃_1} {f₂₄_1 : X₂_1 ⟶ X₄_1} {f₃₄_1 : X₃_1 ⟶ X₄_1}
  {fac_1 : CategoryTheory.CategoryStruct.comp f₁₂_1 f₂₄_1 = CategoryTheory.CategoryStruct.comp f₁₃_1 f₃₄_1},
  { X₁ := X₁, X₂ := X₂, X₃ := X₃, X₄ := X₄, f₁₂ := f₁₂, f₁₃ := f₁₃, f₂₄ := f₂₄, f₃₄ := f₃₄, fac := fac } =
      { X₁ := X₁_1, X₂ := X₂_1, X₃ := X₃_1, X₄ := X₄_1, f₁₂ := f₁₂_1, f₁₃ := f₁₃_1, f₂₄ := f₂₄_1, f₃₄ := f₃₄_1,
        fac := fac_1 } →
    X₁ = X₁_1 ∧ X₂ = X₂_1 ∧ X₃ = X₃_1 ∧ X₄ = X₄_1 ∧ f₁₂ ≍ f₁₂_1 ∧ f₁₃ ≍ f₁₃_1 ∧ f₂₄ ≍ f₂₄_1 ∧ f₃₄ ≍ f₃₄_1