(fmod LengthOfFiniteLists is
  sorts Nat NatList NatIList .
  subsort NatList < NatIList .
  op 0 : -> Nat .
  op s : Nat -> Nat .
  op zeros : -> NatIList .
  op nil : -> NatList .
  op cons : Nat NatIList -> NatIList [strat (1 0)] .
  op cons : Nat NatList -> NatList [strat (1 0)] .
  op length : NatList -> Nat .
  vars M N : Nat .
  var IL : NatIList .
  var L : NatList .
  eq zeros = cons(0,zeros) .
  eq length(nil) = 0 .
  eq length(cons(N,L)) = s(length(L)) .
endfm)