  Symbolic execution uses various algorithms (matching, (anti)unification),
whose executions are parameters for proof object generation. This paper
proposes a generic method for generating proof objects for such parameters. We
present in detail how our method works for the case of antiunification. The
approach is accompanied by an implementation prototype, including a proof
object generator and a proof object checker. In order to investigate the size
of the proof objects, we generate and check proof objects for inputs inspired
from the K definitions of C and Java.
