A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem