We use Raoult's principle of open induction to give a constructive proof of Higman's Lemma. In contrast to previous proofs, our proof directly uses the property that every infinite sequence has an infinite ordered subsequence. This straightens the inductive argument at the cost of a more complex order.
List of Keywords: Wellfounded order. Open induction. Complete partial order, Higman's Lemma, Kruskal's Tree Theorem.
Ulrike Peiker, Martin Griebl