t:Term. s(t) 
Termt:Term. f(t) Terms,v:Term. t[s/v] = tt:Term. closed(t) Prop| Some definitions of interest. | |
| s | Def s(t) == f(t)/q(f(t)) |
| Thm* t:Term. s(t) Term | |
| f | Def f(t) == SUBX(q(t); SUBX(X; Q(X))) |
| Thm* t:Term. f(t) Term | |
| term_closed | Def closed(t) == s,v:Term. t[s/v] = t |
| Thm* t:Term. closed(t) Prop |
About:
 |  |  |  |  |