Q: What is a subterm?
A: Section 3.2 of the textbook defines syntax and seems to think that "subterm" is obvious. I thought it was obvious too. A subterm is a term that occurs inside of another term. Example:
(succ 0) in (pred succ 0)
Q: Is the subterm relation reflexive?
A: Yes. Subterms that are not equal are called proper subterms.
Q: Can you give more examples?
A: Yes. The term succ if iszero 0 then true else pred false has the following subterms:
The following are NOT subterms:succ if iszero 0 then true else pred false if iszero 0 then true false pred false iszero 0 0 true pred false false
succ succ if iszero 0 then true else pred false if true then true else pred false succ iszero 0 succ 0 succ true
Q: But that term is badly typed!
A: Yes. And why is that a problem?
The concept of subterms has nothing to do with evaluation or typing or values. You're supposed to prove that subterms of typed terms are typed too. If you only accepted typed terms, the proof would be different and maybe' even more trivial.