addAllInstancesOfSigs addInstancesOfSig addInstancesOfSigs addTInstName allQIdsOfAssert allQIdsOfAsserts allQIdsOfSigs allQIdsOfTerm allSigs emptyTPSubst isTypeParameter matchSort matchSorts nameOfSig parent ppCmd ppSigBody prettyVar qidName reduceAsInTerm rnmDefSig rnmFunSig rnmQId rnmQIdWithTInst rnmQIdWithTInstTerm rnmTerm sAssert showSMT showSMTRaw showSort sigNameSort sigTypeAsSort simpTerm sortIdsOfSort sortOfSortedVar sortedConst sortsOfTerm substDefSig substFunSig substQId substSV substSort substTerm tComb tConj tDisj tEqu tEquVar tFalse tNot tTrue toTInstName typeParamsOfFunSig typeParamsOfQId typeParamsOfSV typeParamsOfSort typeParamsOfTerm unpoly