⁵Note that here we assume the declaration of the NatSeq concatenation operator __ as given in page 45, where it is declared to be associative. If we consider the declaration of this operator given in page 72, which is also declared to have nil as identity element, then we should write this equation as

  op _occurs-inner_: [Nat] [NatSeq] -> [Bool] .

  ceq N:Nat occurs-inner NS:NatSeq = true

     if (I:Nat NS0:NatSeq N:Nat NS1:NatSeq M:Nat) := NS:NatSeq .

since the variables NS0:NatSeq and NS1:NatSeq might be instantiated to nil.