{i n : ℕ} →
  (SimplexCategory.mk i ⟶ SimplexCategory.mk n) →
    autoParam (i ≤ 2) SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂._auto_1 →
      CategoryTheory.StructuredArrow (Opposite.op (SimplexCategory.mk n)) (SimplexCategory.Truncated.inclusion 2).op