nil ; h.l' h.(LShort(l') \ h) (recursive)
Thm* 
St:Type, l:St*, eq:(St
St
). LShort(l) 
St*
nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi
(recursive)
Thm* St:Type, l:St*, s:St, eq:(StSt). (l \ s) St*
| lshort |
Def LShort(l) == Case of l; nil nil ; h.l' h.(LShort(l') \ h) (recursive)
Thm* |
| lremove |
Def l \ a == Case of l; nil nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi
(recursive)
Thm* |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |