Higman's Lemma is basic to well-quasi-ordering (WQO) theory, but has many specific forms, for example: the Cartesian product of two WQOs is a WQO. Any new extensions?

Usually proved by minimal bad sequence arguments.   Besides Cartesian product Higman (a),
There is Higman (b) re injective order-preserving finite subsequences, and Higman (c)
which says that if Q is a WQO then the finite subsets of Q are WQO by injective order-preserving maps.  There could be further Higman (d) and beyond.