それだと、Prove(x) (⇔ヨyproof(x,y) )が再帰的でないのと同様に、IsTerm (x)も再帰的でなくなってしまうような気がするのですが。

理解力がなく申し訳ないです。
身近に教えてくれる人がいればいいのですが、なにぶん独学なもので。。。
また明日しっかり考えてみようと思います。今日はご丁寧にありがとうございました。