Iso-recursive types and equi-recursive types are two common approaches to recursive types. However, understanding the relationship between these two formulations, both in static typing and dynamic semantics, has long been a research problem. Previous attempts to tackle this issue have involved complicated rules and proofs. In this session, we will explore the possibility of finding a simpler solution for this problem, leveraging the advantages of the full iso-recursive type system discussed in our previous seminar.