∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.ForwardPatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos →
    (∀ (pos' : s.Pos), pos < pos' → ¬String.Slice.Pattern.Model.IsMatch pat pos') →
      String.Slice.Pattern.Model.IsLongestMatch pat pos