TRS:
 {       first(0(), X) -> nil(),
  first(s(X), cons(Y)) -> cons(Y),
               from(X) -> cons(X)}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(from) = [1], pi(first) = [1,2]
  
Safe:
   
  
Predicative System:
   {         first(0(),X;) -> nil(),
    first(s(X;),cons(Y;);) -> cons(Y;),
                  from(X;) -> cons(X;)}
  

   
  

  Qed