Explained in CoinductiveDataType