Agda-2.3.2.2: test/fail/TerminationRecordPatternCoerce.err
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)