Session types provide a principled programming discipline for structured interactions. They are used to
statically check the safety of protocol composition and the absence of communication errors. These properties
depend upon the meta-theory of the typing discipline, usually a type safety proof. These proofs, while
conceptually simple, are very delicate and error prone due to the presence of linearity and name passing and
have been falsified in several works in the literature. In this work, we explore mechanised proofs in theorem
assistants as tools to develop trustworthy proofs, and at the same time to guide extensions that do not violate
type safety. To that end, we study the meta-theory of two of the most used binary session types systems,
the Honda-Vasconcelos-Kubo system and the more flexible revisited system by Yoshida and Vasconcelos.
Additionally, we show the subtlety of representing the first system in α-equivalent representations.We develop
these proofs in the Coq proof assistant, using a locally nameless representation for binders, and small scale
reflection and overloaded lemmas to simplify the handling of linear typing environments.