Induction in soundness proof

[rzach]

• in the section on soundness in the Metatheory chapter, there is what appears to be an orphaned reference to the principle of strong induction: "Note that this proof appeals to a principle of strong induction on the length of TFL-proofs. This is the first time we have seen that principle, and you should pause to confirm that it is, indeed, justified." Nothing else is said about induction in the textbook
• forall x distinguishes between premises and assumptions, and so this proof should too