{X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op (SimplexCategory.mk 0))} →
      {f g : X.PtSimplex n x} →
        {i : Fin (n + 1)} →
          {motive : f.RelStruct g i → Sort u_1} →
            (t : f.RelStruct g i) →
              ((map : SSet.stdSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ X) →
                  (δ_castSucc_map : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) map = f.map) →
                    (δ_succ_map : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) map = g.map) →
                      (δ_map_of_lt :
                          ∀ j < i.castSucc,
                            CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x) →
                        (δ_map_of_gt :
                            ∀ (j : Fin (n + 2)),
                              i.succ < j →
                                CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x) →
                          motive
                            { map := map, δ_castSucc_map := δ_castSucc_map, δ_succ_map := δ_succ_map,
                              δ_map_of_lt := δ_map_of_lt, δ_map_of_gt := δ_map_of_gt }) →
                motive t