no goals
l m r : List Char
p : Nat
⊢ Substring.atEnd
        { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }
        { byteIdx := p } =
      true ↔
    p = utf8Len m
simp [Substring.atEnd, Pos.ext_iff, Nat.add_left_cancel_iff]