Def (rec) l \ a == Case of l : null nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi

Thm* l:St*, s:St, eq:(StSt). (l \ s) St*