Termination checking failed for the following functions:
  f, f'
Problematic calls:
  f (isCons (tl h t)) (tl h t) refl
    (at TerminationRecordPatternCoerce.agda:44,32-33)
  f' (isCons (tl b' h t p)) (tl b' h t p) refl
    (at TerminationRecordPatternCoerce.agda:56,27-29)