∀ {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := 1 }, property := SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.σ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2
          SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1)
        h) =
    CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.σ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
          SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
        h)