[Agda] the recursive definition can not terminate

[mo jia]

Hi.

I am doing the exercise from the chapter 3 in https://plfa.github.io/Relations/.

The last one:

Can x
---------------
to (from x) ≡ x

seem too difficult for me using what the book said in first 3 chapters.

I have the last try:  use t1 and t2  recursive declaration.

I got error like this:

Termination checking failed for the following functions:
  t2, t1
Problematic calls:
  t1 (x1 x) x1 cx One1
    (at /Users/jiamo/agda/ylib/src/ylib/can.agda:146,39-41)
  t2 (x0 x) x0 cx One1
    (at /Users/jiamo/agda/ylib/src/ylib/can.agda:156,30-32)

The total agda file is self-sufficiency for someone have interest to
have a look.

https://gist.github.com/jiamo/af8cd8dd5a4702f81ca6dde04f8e00de

And I still wonder this problem should have a very simple answer like
what I do for

can_inc : ∀ {x : Bin}
→ Can x
-------------
→ Can (inc x)
can_inc {_} (Can_One cx) = Can_One(one_inc cx)
can_inc { (x0 nil) } (Can_Zero) = Can_One(One1)

Appreciate for any suggestion.