Operational Game Semantics (OGS) is a method for building trace models for higher-order languages based on ideas from pointer games—most importantly keeping traces first-order. These models are typically proven sound (and sometimes complete) w.r.t. contextual equivalence. We present a formal treatment of this technique in the Coq proof assistant, abstracting away the specifics of the modelled language and develop an abstract account of OGS, expliciting the hypotheses needed for the soundness proof to go through. In this talk, we propose (1) a brief rundown on operational game semantics, (2) a high-level view of our contributions, and finally (3) a more technical elaboration of a specific aspect of the correctness proof, namely well-definedness of the composition of Proponent- and Opponent-strategies. Indeed, this crucial point involves the so-called infinite chit-chat problem, to which we provide an abstract solution we believe may interest the GALOP audience.