Solution

ID: past-exam-of-the-logic-and-set-theory-course-of-the-university-of-oxford/2011/a/3/b/ii/solution

Take . The term is free for substitution for : its variable is not bound by the enclosing quantifier. The term is not free for substitution for , because insertion under captures that occurrence.
Thus the first substitution gives ; the second, illegitimate substitution would give .

New to topics? Read the docs here!