Yannick Forster, Felix Jahn, Gert Smolka: A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). CPP 2023: 159-166