f(t))
t:Term. s(t) 
Termt; SUBX(X; UP(X)))t:Term. f(t) Terms,v:Term. t[s/v] = tt:Term. closed(t) Prop| Some definitions of interest. | |
| s | Def s(t) == SUBX(f(t); f(t)) |
| Thm* t:Term. s(t) Term | |
| f | Def f(t) == SUBX(t; SUBX(X; UP(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:
 |  |  |  |  |