Proof pearl: a formal proof of Higman's lemma in ACL2
scientific article; zbMATH DE number 6062053