fmod CDR is 
	sorts MyItem MyList MyNat InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op cdr : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z F : MyItem .

	*** eq cdr([]) =  [].
	eq cdr(cons(Y,[])) = [] .
	eq cdr(cons(X,cons(Y,[]))) = cons(Y, []) .
	eq cdr(cons(Y,cons(X,cons(Z,[])))) = cons(X, cons(Z, [])).
	eq cdr(cons(F, cons(Y,cons(X,cons(Z,[]))))) = cons(Y, cons(X, cons(Z, []))).
endfm