∀ {s : String.Slice} (p₁ : s.Pos) {p₂ : s.Pos} (h : p₁ ≤ p₂) (l l_1 : String.Slice.Pattern.Model.SlicesFrom p₂),
  l = l_1 → String.Slice.Pattern.Model.SlicesFrom.extend p₁ h l = String.Slice.Pattern.Model.SlicesFrom.extend p₁ h l_1