Termination checker is sensitive to let-bindings

[knisht]

f and g are actually the same, so there should not be any problems with termination checking.

\data Q
  | q Q

\func g (q : Q) : Q | q q2 => g q2

\func f (q : Q) : Q | q q2 => \let r => q2 \in f r

[valis]

These functions are not the same; they are only equivalent up to computation. Termination checker does not perform any computation. For example, you can write something like this

\func f (n : Nat) : Nat
  | 0 => 0
  | suc n => f (n + some_complicated_expression_that_evaluates_to_0)

Should this also be accepted?

[ice1000]

This is not accepted in Agda: https://tio.run/##S0xPSfz/P78gNU8hM7cgv6hEwREooudUmplTkpmn55dYwsWVpmClAGQo6NqBKCDXQMFWwQBIaxSXJiskagJ5QLaGgYK2goEmkEjU/P8fAA