TRS:
 {      fst(0(), Z) -> nil(),
  fst(s(), cons(Y)) -> cons(Y),
            from(X) -> cons(X),
        add(0(), X) -> X,
        add(s(), Y) -> s(),
         len(nil()) -> 0(),
       len(cons(X)) -> s()}
 POP*:
  Quasi-Precedence:
  len > 0 ~ nil, 
  len > s, 
  from > cons
  0 ~ nil
  
Normal:
   pi(len) = [1], pi(from) = [1], pi(fst) = [1,2]
  
Safe:
   pi(cons) = [1]
  
Predicative System:
   {       fst(0(),Z;) -> nil(),
    fst(s(),cons(;Y);) -> cons(;Y),
              from(X;) -> cons(;X),
           add(0(),X;) -> X,
           add(s(),Y;) -> s(),
           len(nil();) -> 0(),
        len(cons(;X);) -> s()}
  Qed