I like thinking about “witness data” https://www.philipzucker.com/proof_objects/ . Given the witness data, some problem becomes easier in some sense to do (often an improvement in decidability or big O complexity, but I also accept a subjective “just becomes easier to think about”). Some examples of such data

[...]

• The witness an object is in a list is the index at which to find it.

Witnesses are somewhat related to “parse don’t validate”. Parse trees are witness data to a string being in a language.

Thinnings are witnesses to a sublist question.

I can write a function to determine if one list is a sublist of another (or subsequence really. My brain doesn’t distinguish between the words, but many brains do). Traverse through the big one and increment a pointer into the small one when we find a match

[...]

But I can also do so in a witness producing way. This is in some sense a trace of the computation

[...]

Thinnings can also be used as instructions on how to produce the small list from the big list

[...]

There can be multiple possible certificates in the presence of duplicates. Our proof producing method only produces one of them (a lex minimal one kind of).