{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      {motive : X.ExtraDegeneracy → Sort u} →
        (t : X.ExtraDegeneracy) →
          ((s' :
                CategoryTheory.SimplicialObject.Augmented.point.obj X ⟶
                  (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj (Opposite.op (SimplexCategory.mk 0))) →
              (s :
                  (n : ℕ) →
                    (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj (Opposite.op (SimplexCategory.mk n)) ⟶
                      (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj
                        (Opposite.op (SimplexCategory.mk (n + 1)))) →
                (s'_comp_ε :
                    CategoryTheory.CategoryStruct.comp s' (X.hom.app (Opposite.op (SimplexCategory.mk 0))) =
                      CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialObject.Augmented.point.obj X)) →
                  (s₀_comp_δ₁ :
                      CategoryTheory.CategoryStruct.comp (s 0) (X.left.δ 1) =
                        CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) s') →
                    (s_comp_δ₀ :
                        ∀ (n : ℕ),
                          CategoryTheory.CategoryStruct.comp (s n) (X.left.δ 0) =
                            CategoryTheory.CategoryStruct.id
                              ((CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj
                                (Opposite.op (SimplexCategory.mk n)))) →
                      (s_comp_δ :
                          ∀ (n : ℕ) (i : Fin (n + 2)),
                            CategoryTheory.CategoryStruct.comp (s (n + 1)) (X.left.δ i.succ) =
                              CategoryTheory.CategoryStruct.comp (X.left.δ i) (s n)) →
                        (s_comp_σ :
                            ∀ (n : ℕ) (i : Fin (n + 1)),
                              CategoryTheory.CategoryStruct.comp (s n) (X.left.σ i.succ) =
                                CategoryTheory.CategoryStruct.comp (X.left.σ i) (s (n + 1))) →
                          motive
                            { s' := s', s := s, s'_comp_ε := s'_comp_ε, s₀_comp_δ₁ := s₀_comp_δ₁,
                              s_comp_δ₀ := s_comp_δ₀, s_comp_δ := s_comp_δ, s_comp_σ := s_comp_σ }) →
            motive t