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. 
Christian Sternagel
cs.LO