∀ {X : SSet} {d : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk d)))
  (y : X.obj (Opposite.op (SimplexCategory.mk (d + 1))))
  (f : SimplexCategory.mk { dim := d, simplex := x }.dim ⟶ SimplexCategory.mk { dim := d + 1, simplex := y }.dim)
  (motive :
    CategoryTheory.Mono f ∧ X.map f.op { dim := d + 1, simplex := y }.simplex = { dim := d, simplex := x }.simplex →
      Prop)
  (x_1 :
    CategoryTheory.Mono f ∧ X.map f.op { dim := d + 1, simplex := y }.simplex = { dim := d, simplex := x }.simplex),
  (∀ (h₃ : CategoryTheory.Mono f)
      (h₄ : X.map f.op { dim := d + 1, simplex := y }.simplex = { dim := d, simplex := x }.simplex), motive ⋯) →
    motive x_1