{S : SSet} →
  {motive : S.Quasicategory → Sort u} →
    (t : S.Quasicategory) →
      ((hornFilling' :
            ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : (SSet.horn (n + 2) i).toSSet ⟶ S),
              0 < i → i < Fin.last (n + 2) → ∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.horn (n + 2) i).ι σ) →
          motive ⋯) →
        motive t