Fail Check fix f (x : nat) := (let x := (f x) in f 0).