obj Ex1_2_Luc02c is
  sort S .
  op 2nd : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op from : S -> S .
  op s : S -> S .
  vars X Y Z : S .
  eq 2nd(cons(X,cons(Y,Z))) = Y .
  eq from(X) = cons(X,from(s(X))) .
endo