fix substitution for ifs; add the proof that there is no term V
with Yx. x \Downarrow V.