bs ; a.as' [a / (as' @ bs)] (recursive)
T:Type, as,bs:T List. (as @ bs) 
T List| Who Cites term vars? | |
| term_vars | Def term_vars(t) == iterate(statevar v- > [v] statevar v'- > [v] funsymbol f- > nil freevar f- > nil trace(P)- > nil x(y)- > x @ y over t) |
| append |
Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive) |
|
Thm* T:Type, as,bs:T List. (as @ bs) T List |
About:
 |  |  |  |  |
 |  |  |  |  |