Changed the whole project to remove 0-arity schematic variables and replace them by variables. It compiles, but at least one proof doesn't go through.