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.