YES
TRS:
 {       first(0(), X) -> nil(),
  first(s(X), cons(Y)) -> cons(Y),
               from(X) -> cons(X)}
 RUF:
  Strict:
   {}
  Weak:
   {}
  Qed