Undecidability of Dyadic First-Order Logic in Coq Academic Article