∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : CategoryTheory.SimplicialObject C} {n : ℕ}
  [self : X.IsCoskeletal n],
  CategoryTheory.Functor.IsRightKanExtension X
    (CategoryTheory.CategoryStruct.id ((SimplexCategory.Truncated.inclusion n).op.comp X))