WrongSizeAssignment2.err

Termination checking failed for the following functions:
  f
Problematic calls:
  f {i} (suc {i} (lift {i} x))
    (at WrongSizeAssignment2.agda:25,7-8)