"bool" "bool" var varType varTerm "bool" const "bool" typeOp nil opType constTerm refl absThm