"x" const "bool" typeOp nil opType constTerm assume 1 def 1 remove deductAntisym