∀ (motive : (x₁ y₁ x₂ y₂ : AugmentedSimplexCategory) → (x₁ ⟶ y₁) → (x₂ ⟶ y₂) → Prop)
  (x₁ y₁ x₂ y₂ : AugmentedSimplexCategory) (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂),
  (∀ (x₁ y₁ x₂ y₂ : SimplexCategory) (f₁ : CategoryTheory.WithInitial.of x₁ ⟶ CategoryTheory.WithInitial.of y₁)
      (f₂ : CategoryTheory.WithInitial.of x₂ ⟶ CategoryTheory.WithInitial.of y₂),
      motive (CategoryTheory.WithInitial.of x₁) (CategoryTheory.WithInitial.of y₁) (CategoryTheory.WithInitial.of x₂)
        (CategoryTheory.WithInitial.of y₂) f₁ f₂) →
    (∀ (x x_1 x_2 : AugmentedSimplexCategory) (f₁ : CategoryTheory.WithInitial.star ⟶ x) (f₂ : x_1 ⟶ x_2),
        motive CategoryTheory.WithInitial.star x x_1 x_2 f₁ f₂) →
      (∀ (x x_1 x_2 : AugmentedSimplexCategory) (x_3 : x ⟶ x_1) (x_4 : CategoryTheory.WithInitial.star ⟶ x_2),
          motive x x_1 CategoryTheory.WithInitial.star x_2 x_3 x_4) →
        motive x₁ y₁ x₂ y₂ f₁ f₂