A coinduction principle for recursive data types based on bisimulation
scientific article; zbMATH DE number 930738