Termination checking failed for the following functions:
  f
Problematic calls:
  f inf d₂
    (at BadTermination.agda:16,19-20)