∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.ForwardPattern pat}
  [self : String.Slice.Pattern.LawfulForwardPattern pat] (s : String.Slice),
  String.Slice.Pattern.ForwardPattern.startsWith pat s = (String.Slice.Pattern.ForwardPattern.dropPrefix? pat s).isSome