Formal proofs of the meta-theory of programming calculi are important tools to develop a trust-worthy theoretical base. The meta-theory of systems with session types is delicate and error prone. I will talk about an approach to mechanise such proofs in the Coq proof assistant. In particular, I want to discuss some subtle aspects around the adequacy around a particular choice of representation, in particular some lessons learned in the process. And finally, offer a glimpse on the things we want to try in the future. This is joint work with Nobuko Yoshida.