Undecidability of Higher-Order Unification Formalised in Coq

POPL 2020