Proof obligations for monomorphicity

In certain applications of formal methods to development of correct
software one wants the requirement specification to be monomorphic,
i.e. that every two term-generated models of it are isomorphic.
Consequently, the question arises how to guarantee monomorphicity
(which is not decidable in general). In this paper we show that the
task of proving monomorphicity of a specification can be reduced to a
task of proving certain properties of procedures (with indeterministic
constructs). So this task can be directly dealt with in the KIV
system (Karlsruhe Interactive Verifier) which was originally designed
for software verification. We prove correctness and completeness of
our method.