∀ {motive : ⦃X Y : SimplexCategoryGenRel⦄ → (x : X ⟶ Y) → SimplexCategoryGenRel.degeneracies x → Prop}
  ⦃X Y : SimplexCategoryGenRel⦄ {x : X ⟶ Y} (t : SimplexCategoryGenRel.degeneracies x),
  (∀ {n : ℕ} (i : Fin (n + 1)), motive (SimplexCategoryGenRel.σ i) ⋯) → motive x t