Session types express a protocol which specifies the order and type of messages exchanged by concurrently executing processes. Prior work has been adapted to many frameworks including Agha’s work [10], which has successfully extended session types to model distributed asynchronous multi-actors. Most works on session types, including Agha’s work, take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. One main problem of an equi-recursive type system is that its mechanisation in proof assistants is utterly complex and eventually requires co-induction. To overcome this problem, this paper presents an iso-recursive type system for binary sessions based on a novel congruence on types which relates recursive types and their unfolding. Our system based on type congruence enables to use a simple syntactic-directed duality without complicating the typability of processes. We mechanise the type congruence relation in Rocq without resorting to coinductive types, and use the proof assistant to show that our iso-recursive typing system satisfies subject reduction.