Better handling of stuck terms?

[favonia]

I am not very satisfied with the warnings here. Perhaps we should plug the terms in focus back to the stack frames for pretty-printing? And a stuck term should be treated as a fatal error.

data S1' : (U 0 kan)
  { base'
  , loop' [x : dim] [x=0 (self base')] [x=1 (self base')]
  }
by {
  auto
}.

theorem Test :
  (=
   S1
   (S1-rec [_] S1 (. S1' base') base [u] (loop u))
   base)
by {
  auto; ?
}.