Corrected bug in substitution and in conversion, higher-order unification seems to work.