Ike Mulder, Robbert Krebbers: Unification for Subformula Linking under Quantifiers. CPP 2024: 75-88