Def (rec) LShort(l) == Case of l : null nil ; h.l' h.(LShort(l') \ h)

Thm* l:St*, eq:(StSt). LShort(l) St*

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*