simplified Unif a bit
simplified a case of the completeness logical relation
type renamings/substitutions are inferrable in the definitions of term renamings/substitutions