Termination checking failed for the following functions: loop Problematic calls: loop False foo (at CoinductionAndUnivalence.agda:44,1-5)