{ρ : Type} →
  {pat : ρ} →
    {P : Sort u} →
      {dropSuffix? : (s : String.Slice) → Option s.Pos} →
        {dropSuffixOfNonempty? : (s : String.Slice) → s.isEmpty = false → Option s.Pos} →
          {endsWith : String.Slice → Bool} →
            {dropSuffix?' : (s : String.Slice) → Option s.Pos} →
              {dropSuffixOfNonempty?' : (s : String.Slice) → s.isEmpty = false → Option s.Pos} →
                {endsWith' : String.Slice → Bool} →
                  { dropSuffix? := dropSuffix?, dropSuffixOfNonempty? := dropSuffixOfNonempty?, endsWith := endsWith } =
                      { dropSuffix? := dropSuffix?', dropSuffixOfNonempty? := dropSuffixOfNonempty?',
                        endsWith := endsWith' } →
                    (dropSuffix? = dropSuffix?' →
                        dropSuffixOfNonempty? = dropSuffixOfNonempty?' → endsWith = endsWith' → P) →
                      P