"n" "abs" "rep" "xtype" nil cons "x" "xtype" varType var "c" const "bool" typeOp nil opType 1 def constTerm absTerm "a" const 1 remove constTerm appTerm assume defineTypeOp