A Locale for Minimal Bad Sequences

We present a locale that abstracts over the necessary ingredients for constructing a minimal bad sequence, as required in classical proofs of Higman’s lemma and Kruskal’s tree theorem.